Factoring the first analytic R-322 block

The analytic schedule places an innermost primitive block at its head. This file makes the first pointwise separation needed by the collapse induction:

• later difference factors only read coordinates outside the head block;
• an unreplaced chain edge whose two vertices avoid the head block is likewise independent of the head variables;
• the head difference is the literal difference of the two endpoint kernels with their common, external successor;
• consequently the generalized signed Green skeleton factors into a local head part and an outer part which is constant in all head-block variables.

The chain family is kept heterogeneous. Thus the statement remains usable after earlier primitive blocks have already been replaced by collapsed kernels; no free-Green specialization is hidden in the induction interface.

Generalized analytic skeleton

def Anderson4D.r322JChainEdgeLeft {n : ℕ} (e : Fin (n - 1)) : Fin n

Left vertex of an internal J chain edge.

Equations

• Anderson4D.r322JChainEdgeLeft e = ⟨↑e, ⋯⟩

def Anderson4D.r322JChainEdgeRight {n : ℕ} (e : Fin (n - 1)) : Fin n

Right vertex of an internal J chain edge.

Equations

• Anderson4D.r322JChainEdgeRight e = ⟨↑e + 1, ⋯⟩

def Anderson4D.R322ChainEdgeOutside {n : ℕ} (B : Finset (Fin n)) (e : Fin (n - 1)) : Prop

A chain edge is exterior to a block when both of its coordinate reads are outside the block.

Equations

• Anderson4D.R322ChainEdgeOutside B e = (Anderson4D.r322JChainEdgeLeft e ∉ B ∧ Anderson4D.r322JChainEdgeRight e ∉ B)

@[implicit_reducible]

instance Anderson4D.instDecidableR322ChainEdgeOutside {n : ℕ} (B : Finset (Fin n)) (e : Fin (n - 1)) : Decidable (R322ChainEdgeOutside B e)

Equations

• Anderson4D.instDecidableR322ChainEdgeOutside B e = id inferInstance

noncomputable def Anderson4D.r322AnalyticChainEdgeFactorWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (x : Fin n → T4) (e : Fin (n - 1)) : ℝ

One generalized chain factor, with analytically scheduled right edges removed exactly as in the closed J formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.r322AnalyticChainProductWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (x : Fin n → T4) : ℝ

Product of all generalized, unreplaced chain edges.

Equations

• Anderson4D.r322AnalyticChainProductWith G κ x = ∏ e : Fin (n - 1), Anderson4D.r322AnalyticChainEdgeFactorWith G κ x e

noncomputable def Anderson4D.r322AnalyticDiffProductWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (steps : List (R322ExtractionStep n)) (x : Fin n → T4) : ℝ

Difference-factor product for an arbitrary suffix of the analytic schedule.

Equations

• Anderson4D.r322AnalyticDiffProductWith G steps x = (List.map (fun (t : Anderson4D.R322ExtractionStep n) => Anderson4D.diffFactorJWith G x t.1) steps).prod

noncomputable def Anderson4D.r322AnalyticSkeletonWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (x : Fin n → T4) : ℝ

The closed analytic skeleton with heterogeneous chain inputs.

Equations

• Anderson4D.r322AnalyticSkeletonWith G κ x = Anderson4D.r322AnalyticChainProductWith G κ x * Anderson4D.r322AnalyticDiffProductWith G (Anderson4D.r322AnalyticSchedule κ) x

theorem Anderson4D.r322AnalyticSkeletonWith_green_eq {n : ℕ} (κ : PartialPairing (Fin n)) (x : Fin n → T4) : r322AnalyticSkeletonWith (fun (x : Fin (n - 1)) => greenFn) κ x = r322AnalyticGreenSkeleton κ x

At the constant Green family, the generalized skeleton is the frozen analytic Green skeleton.

Coordinate independence of the two outer ingredients

theorem Anderson4D.jChainEdgeWith_eq_of_eq_outside_analyticHeadBlock {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (x y : Fin n → T4) (s : R322ExtractionStep n) (e : Fin (n - 1)) (he : R322ChainEdgeOutside s.2 e) (hxy : ∀ i ∉ s.2, x i = y i) : jChainEdgeWith G x e = jChainEdgeWith G y e

A generalized chain edge whose two vertices avoid the head block is unchanged when only head-block coordinates move.

theorem Anderson4D.r322AnalyticUnreplacedChainEdgeFactor_eq {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (x y : Fin n → T4) (s : R322ExtractionStep n) (e : Fin (n - 1)) (he : R322ChainEdgeOutside s.2 e) (hunreplaced : ↑e ∉ List.map (fun (t : R322ExtractionStep n) => ↑t.1.2) (r322AnalyticSchedule κ)) (hxy : ∀ i ∉ s.2, x i = y i) : r322AnalyticChainEdgeFactorWith G κ x e = r322AnalyticChainEdgeFactorWith G κ y e

In particular, an unreplaced exterior analytic chain factor is head-coordinate independent.

theorem Anderson4D.r322AnalyticTailDiffProductWith_eq {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (x y : Fin n → T4) (s : R322ExtractionStep n) (tail : List (R322ExtractionStep n)) (hschedule : r322AnalyticSchedule κ = s :: tail) (hxy : ∀ i ∉ s.2, x i = y i) : r322AnalyticDiffProductWith G tail x = r322AnalyticDiffProductWith G tail y

The whole product of later analytic differences is independent of the head-block variables.

Local/outer chain split

noncomputable def Anderson4D.r322AnalyticHeadLocalChainProductWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (s : R322ExtractionStep n) (x : Fin n → T4) : ℝ

Chain factors touching the head block. Replaced edges remain literal ones, so this is an exact factor of the closed skeleton.

Equations

• Anderson4D.r322AnalyticHeadLocalChainProductWith G κ s x = ∏ e : Fin (n - 1), if Anderson4D.R322ChainEdgeOutside s.2 e then 1 else Anderson4D.r322AnalyticChainEdgeFactorWith G κ x e

noncomputable def Anderson4D.r322AnalyticHeadOuterChainProductWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (s : R322ExtractionStep n) (x : Fin n → T4) : ℝ

Chain factors whose two vertices both avoid the head block.

Equations

• Anderson4D.r322AnalyticHeadOuterChainProductWith G κ s x = ∏ e : Fin (n - 1), if Anderson4D.R322ChainEdgeOutside s.2 e then Anderson4D.r322AnalyticChainEdgeFactorWith G κ x e else 1

theorem Anderson4D.r322AnalyticChainProductWith_eq_local_mul_outer {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (s : R322ExtractionStep n) (x : Fin n → T4) : r322AnalyticChainProductWith G κ x = r322AnalyticHeadLocalChainProductWith G κ s x * r322AnalyticHeadOuterChainProductWith G κ s x

The full generalized chain product is the product of the touching and exterior parts.

theorem Anderson4D.r322AnalyticHeadOuterChainProductWith_eq {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (x y : Fin n → T4) (s : R322ExtractionStep n) (hxy : ∀ i ∉ s.2, x i = y i) : r322AnalyticHeadOuterChainProductWith G κ s x = r322AnalyticHeadOuterChainProductWith G κ s y

The exterior chain product is independent of all head-block coordinates, whether an exterior edge is replaced or unreplaced.

The explicit head difference

theorem Anderson4D.r322AnalyticHead_diffFactorJWith_eq {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (x : Fin n → T4) (s : R322ExtractionStep n) (hs : ExtractionPairBlockAligned s.1 s.2) (hguard : ↑s.1.2 + 1 < n) : ⟨↑s.1.2 + 1, hguard⟩ ∉ s.2 ∧ diffFactorJWith G x s.1 = G ⟨↑s.1.2, ⋯⟩ (x s.1.2 - x ⟨↑s.1.2 + 1, hguard⟩) - G ⟨↑s.1.2, ⋯⟩ (x s.1.1 - x ⟨↑s.1.2 + 1, hguard⟩)

In the proper guarded case, the head difference is exactly the difference of the two endpoint kernels evaluated against their common successor. The successor is outside the head block.

Pointwise head factorization

noncomputable def Anderson4D.r322AnalyticHeadLocalFactorWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (s : R322ExtractionStep n) (x : Fin n → T4) : ℝ

The local part: every chain edge touching the head block and the signed head endpoint difference.

Equations

• Anderson4D.r322AnalyticHeadLocalFactorWith G κ s x = Anderson4D.r322AnalyticHeadLocalChainProductWith G κ s x * Anderson4D.diffFactorJWith G x s.1

noncomputable def Anderson4D.r322AnalyticHeadOuterFactorWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (s : R322ExtractionStep n) (tail : List (R322ExtractionStep n)) (x : Fin n → T4) : ℝ

The outer part: all fully exterior chain edges and all later analytic differences.

Equations

• Anderson4D.r322AnalyticHeadOuterFactorWith G κ s tail x = Anderson4D.r322AnalyticHeadOuterChainProductWith G κ s x * Anderson4D.r322AnalyticDiffProductWith G tail x

theorem Anderson4D.r322AnalyticSkeletonWith_eq_headLocal_mul_outer {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (s : R322ExtractionStep n) (tail : List (R322ExtractionStep n)) (x : Fin n → T4) (hschedule : r322AnalyticSchedule κ = s :: tail) : r322AnalyticSkeletonWith G κ x = r322AnalyticHeadLocalFactorWith G κ s x * r322AnalyticHeadOuterFactorWith G κ s tail x

Exact pointwise local/outer factorization of the generalized skeleton at the head of the analytic schedule.

theorem Anderson4D.r322AnalyticHeadOuterFactorWith_eq {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (κ : PartialPairing (Fin n)) (x y : Fin n → T4) (s : R322ExtractionStep n) (tail : List (R322ExtractionStep n)) (hschedule : r322AnalyticSchedule κ = s :: tail) (hxy : ∀ i ∉ s.2, x i = y i) : r322AnalyticHeadOuterFactorWith G κ s tail x = r322AnalyticHeadOuterFactorWith G κ s tail y

The outer factor in the exact split is constant in all head-block variables.

theorem Anderson4D.r322AnalyticGreenSkeleton_eq_headLocal_mul_outer {n : ℕ} (κ : PartialPairing (Fin n)) (s : R322ExtractionStep n) (tail : List (R322ExtractionStep n)) (x : Fin n → T4) (hschedule : r322AnalyticSchedule κ = s :: tail) : r322AnalyticGreenSkeleton κ x = r322AnalyticHeadLocalFactorWith (fun (x : Fin (n - 1)) => greenFn) κ s x * r322AnalyticHeadOuterFactorWith (fun (x : Fin (n - 1)) => greenFn) κ s tail x

Free-Green form of the exact pointwise factorization, connected to the public analytic skeleton.