Schedule closure for the R-322 residual integral #
This module starts by identifying the general sparse-carrier residual step
with the actual first step of endpointFiberDetJSum. The preceding module
already proves the ambient successor translation and the one-step Fubini
update; here the all-Green initial context is connected to that interface
before the schedule induction is assembled.
The first schedule step as a genuine edge-state context #
noncomputable def
Anderson4D.r322InitialProperStepContext
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
Proper-step context carried by the all-Green initial state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Anderson4D.R322InitialProperStepContext.state
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).state = r322InitialAnalyticEdgeState q hq
@[simp]
theorem
Anderson4D.R322InitialProperStepContext.state_edges
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(edge : Fin (2 * q - 1))
:
theorem
Anderson4D.R322InitialProperStepContext.one_le_blockOrder
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
theorem
Anderson4D.R322InitialProperStepContext.standardBlockTuple_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(x : Fin (2 * q) → T4)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).standardBlockTuple x = r322AnalyticProperHeadStandardTuple hq κ hκ head tail hschedule hproper x
The generic sparse block enumeration specializes to the production proper-head enumeration.
theorem
Anderson4D.R322InitialProperStepContext.predecessorVertex_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
r322AnalyticPredecessorVertex (r322InitialProperStepContext hq κ hκ head tail hschedule hproper).state
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).step ⋯ = ⟨↑head.1.1 - 1, ⋯⟩
Initially the greatest active predecessor is the literal ambient vertex
head.left - 1.
theorem
Anderson4D.R322InitialProperStepContext.predecessorEdge_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).predecessorEdge = r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper
theorem
Anderson4D.R322InitialProperStepContext.successorVertex_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).successorVertex = ⟨↑head.1.2 + 1, ⋯⟩
Initially the least active successor is the literal ambient vertex
head.right + 1.
theorem
Anderson4D.R322InitialProperStepContext.outgoingEdge_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
theorem
Anderson4D.R322InitialProperStepContext.internalEdge_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(j : Fin (2 * residualBlockOrder head.2 - 1))
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).internalEdge j = r322AnalyticProperHeadInternalEdge hq κ hκ head tail hschedule hproper j
Every initial internal sparse edge is the corresponding affine proper-head edge.
theorem
Anderson4D.R322InitialProperStepContext.internalEdges_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).internalEdges = fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn
theorem
Anderson4D.R322InitialProperStepContext.predecessorPoint_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(x : Fin (2 * q) → T4)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).predecessorPoint x = x (r322JChainEdgeLeft (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper))
theorem
Anderson4D.R322InitialProperStepContext.successorPoint_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(x : Fin (2 * q) → T4)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).successorPoint x = x ⟨↑head.1.2 + 1, ⋯⟩
theorem
Anderson4D.R322InitialProperStepContext.reconstructBlockTuple_reference_eq
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(z : T4)
(vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4)
(t : Fin (2 * residualBlockOrder head.2) → T4)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).reconstructBlockTuple
(r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC) t = r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC t
Reconstructing the initial head block through the generic sparse-state API is literally the production proper-head reconstruction.
theorem
Anderson4D.R322InitialProperStepContext.ambientLocalIntegrand_eq_headLocal
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(ρ : SmoothCutoff)
(ε : ℝ)
(x : Fin (2 * q) → T4)
:
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).ambientLocalIntegrand ρ ε x = r322AnalyticHeadLocalIntegrandFactor ρ ε κ head tail hschedule x
The state-based ambient local factor is exactly the production analytic-head factor at the all-Green initial state.
The actual initial residual as the first processed state #
Exact order still carried by the suffix after the first analytic schedule block.
Equations
- Anderson4D.r322AnalyticSuffixOrder tail = (List.map (fun (step : Anderson4D.R322ExtractionStep (2 * q)) => Anderson4D.residualBlockOrder step.2) tail).sum
Instances For
theorem
Anderson4D.residualBlockOrder_head_add_suffixOrder
{q : ℕ}
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
:
theorem
Anderson4D.r322InitialResidualIntegrand_reconstruct_eq
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(z : T4)
(vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4)
(t : Fin (2 * residualBlockOrder head.2) → T4)
:
r322InitialResidualIntegrand ρ ε κ head tail hschedule
(r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC t) = (r322InitialProperStepContext hq κ hκ head tail hschedule hproper).ambientLocalIntegrand ρ ε
((r322InitialProperStepContext hq κ hκ head tail hschedule hproper).reconstructBlockTuple
(r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC) t) * r322AnalyticHeadOuterIntegrandFactor ρ ε κ head tail hschedule
(r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC)
At the first block, the exact production residual integrand agrees with the generic sparse-state local factor times the unchanged suffix factor.
theorem
Anderson4D.integral_r322InitialResidualIntegrand_eq_processed
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(z : T4)
(vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4)
:
(∫ (t : Fin (2 * residualBlockOrder head.2) → T4), r322InitialResidualIntegrand ρ ε κ head tail hschedule
(r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC
t) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), (r322InitialProperStepContext hq κ hκ head tail hschedule hproper).processedResidualIntegrand ρ ε
(r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC)
(r322AnalyticHeadOuterIntegrandFactor ρ ε κ head tail hschedule
(r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC))
t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure
The actual first-block integral is exactly the relative-coordinate processed residual integral; the translation is genuine Haar invariance.
noncomputable def
Anderson4D.r322InitialProcessedOuterIntegral
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(z : T4)
:
The exact first processed residual, including the perturbative power carried by every later schedule block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.r322InitialResidualOuterIntegral_eq_processed
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(z : T4)
:
r322InitialResidualOuterIntegral hq ρ lam ε κ hκ head tail hschedule hproper z = r322InitialProcessedOuterIntegral hq ρ lam ε κ hκ head tail hschedule hproper z
The initial residual object from the actual endpoint fibre is exactly
the first generic processed-prefix residual object. In particular, the
global 2q coupling power is neither dropped nor duplicated: it splits
between the head order and the suffix-order ledger.
theorem
Anderson4D.endpointFiberDetJSum_eq_initialProcessedOuterIntegral
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(z : T4)
(hint :
∀ (τ : ReductionEndpointFiberAt κ),
MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure))
:
endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = r322InitialProcessedOuterIntegral hq ρ lam ε κ hκ head tail hschedule hproper z
The endpoint-fibre sum is now connected to the production processed residual API without any model-integrand interface.
noncomputable def
Anderson4D.r322InitialUpdatedOuterIntegral
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(z : T4)
:
The exact residual integral immediately after the first schedule block has been absorbed into its predecessor edge.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.endpointFiberDetJSum_eq_initialUpdatedOuterIntegral
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
(z : T4)
(hint :
∀ (τ : ReductionEndpointFiberAt κ),
MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure))
(hstandard :
∀ᵐ (vC :
{ i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } →
T4) ∂MeasureTheory.Measure.pi
fun (x : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i }) =>
paperMeasure, MeasureTheory.Integrable
((r322InitialProperStepContext hq κ hκ head tail hschedule hproper).localIntegrand ρ ε
((r322InitialProperStepContext hq κ hκ head tail hschedule hproper).predecessorPoint
(r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC) - (r322InitialProperStepContext hq κ hκ head tail hschedule hproper).successorPoint
(r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC)))
(MeasureTheory.Measure.pi
fun
(x :
Fin (2 * residualBlockOrder (r322InitialProperStepContext hq κ hκ head tail hschedule hproper).step.2)) =>
paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))),
MeasureTheory.Integrable
(fun (v : Fin (2 * residualBlockOrder head.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB)
(r322InitialProperStepContext hq κ hκ head tail hschedule hproper).internalEdges
(primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure))
:
endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = r322InitialUpdatedOuterIntegral hq ρ lam ε κ hκ head tail hschedule hproper z
Actual first-step schedule closure.
Starting from endpointFiberDetJSum, the first genuine proper schedule
block is integrated and absorbed into the heterogeneous predecessor edge.
The only premises are the section-integrability statements required by
Fubini; the primitive-endpoint premise is product-Haar almost everywhere,
which is the exact strength supplied by joint integrability.
Continuity with the genuine absorbed-state induction #
theorem
Anderson4D.r322InitialNextState_absorbed
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
R322AnalyticAbsorbedState ρ lam ε hq κ hκ
((r322InitialProperStepContext hq κ hκ head tail hschedule hproper).nextState ρ lam ε)
The state produced by the exact first residual update is the first reachable heterogeneous state of the production schedule.
@[simp]
theorem
Anderson4D.r322InitialNextState_processed
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(head : R322ExtractionStep (2 * q))
(tail : List (R322ExtractionStep (2 * q)))
(hschedule : r322AnalyticSchedule κ = head :: tail)
(hproper : head.1 ≠ r322WholeEndpoint q hq)
:
noncomputable def
Anderson4D.R322AnalyticProperStepContext.nextProperStep
{q : ℕ}
{hq : 1 ≤ q}
(ctx : R322AnalyticProperStepContext q hq)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(next : R322ExtractionStep (2 * q))
(rest : List (R322ExtractionStep (2 * q)))
(hsuffix : ctx.suffix = next :: rest)
(hproper : next.1 ≠ r322WholeEndpoint q hq)
:
Advance a proper-step context to the next proper schedule step using the exact heterogeneous state produced by the current absorption.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Anderson4D.R322AnalyticProperStepContext.nextProperStep_state
{q : ℕ}
{hq : 1 ≤ q}
(ctx : R322AnalyticProperStepContext q hq)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(next : R322ExtractionStep (2 * q))
(rest : List (R322ExtractionStep (2 * q)))
(hsuffix : ctx.suffix = next :: rest)
(hproper : next.1 ≠ r322WholeEndpoint q hq)
:
noncomputable def
Anderson4D.R322AnalyticProperStepContext.nextTerminalStep
{q : ℕ}
{hq : 1 ≤ q}
(ctx : R322AnalyticProperStepContext q hq)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(terminal : R322ExtractionStep (2 * q))
(hsuffix : ctx.suffix = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
:
If only the whole-carrier step remains, the current proper absorption produces the certified terminal context consumed by Proposition 4.1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Anderson4D.R322AnalyticProperStepContext.nextTerminalStep_state
{q : ℕ}
{hq : 1 ≤ q}
(ctx : R322AnalyticProperStepContext q hq)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(terminal : R322ExtractionStep (2 * q))
(hsuffix : ctx.suffix = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
: