Endpoint-signature recovery from primitive block coordinates

The carrier-generic product equivalence only records that every scheduled block is closed and primitive. For the concrete Definition 3.1 schedule we must additionally prove that such a reassembled pairing runs through exactly the same selected relative intervals. This file supplies that selector rigidity and then upgrades the R-322 endpoint fibre to the exact dependent product of primitive coordinates.

Fully paired relative intervals depend only on primitive blocks

theorem Anderson4D.block_subset_of_finsetUnionList_eq {α : Type u_1} [DecidableEq α] {blocks : List (Finset α)} {active B : Finset α} (hcover : finsetUnionList blocks = active) (hB : B ∈ blocks) : B ⊆ active

A block in a finite block cover lies in the covered active carrier.

theorem Anderson4D.isFullyPairedOn_relIcc_of_primitive_block_cover {m : ℕ} (source target : PartialPairing (Fin m)) (blocks : List (Finset (Fin m))) (active : Finset (Fin m)) (hcover : finsetUnionList blocks = active) (hsourceFull : List.Forall (IsFullyPairedOn source) blocks) (hsourcePrimitive : List.Forall (IsRelPrimitiveOn source) blocks) (htargetFull : List.Forall (IsFullyPairedOn target) blocks) (a b : Fin m) (hR : IsFullyPairedOn source (relIcc active a b)) : IsFullyPairedOn target (relIcc active a b)

If two pairings are full on the same block cover and the source pairing is relatively primitive on every block, every source-fully-paired relative interval is also fully paired for the target pairing.

theorem Anderson4D.isRelFullyPaired_iff_of_common_primitive_block_cover {m : ℕ} (κ τ : PartialPairing (Fin m)) (blocks : List (Finset (Fin m))) (active : Finset (Fin m)) (hcover : finsetUnionList blocks = active) (hκFull : List.Forall (IsFullyPairedOn κ) blocks) (hκPrimitive : List.Forall (IsRelPrimitiveOn κ) blocks) (hτFull : List.Forall (IsFullyPairedOn τ) blocks) (hτPrimitive : List.Forall (IsRelPrimitiveOn τ) blocks) (a b : Fin m) : IsRelFullyPaired κ active a b ↔ IsRelFullyPaired τ active a b

Under a common complete primitive block cover, the two pairings have exactly the same relative fully-paired candidates.

Selector recursion from the common block cover

theorem Anderson4D.extractAuxS_final_eq_empty_of_fullyPaired {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (hactive : IsFullyPairedOn κ active) (hcard : active.card ≤ 2 * fuel + 1) : (extractAuxS κ fuel active).2 = ∅

A fully paired active carrier is exhausted whenever the standard two-indices-per-step fuel bound holds.

theorem Anderson4D.finsetUnionList_extractionBlocksAux_eq_active {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (hactive : IsFullyPairedOn κ active) (hcard : active.card ≤ 2 * fuel + 1) : finsetUnionList (extractionBlocksAux κ fuel active) = active

For a fully paired state with sufficient fuel, its concrete extraction blocks cover the active carrier exactly.

theorem Anderson4D.extractAux_eq_of_common_extraction_block_structure {m : ℕ} (κ τ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : IsFullyPairedOn κ active → active.card ≤ 2 * fuel + 1 → List.Forall (IsFullyPairedOn τ) (extractionBlocksAux κ fuel active) → List.Forall (IsRelPrimitiveOn τ) (extractionBlocksAux κ fuel active) → extractAux τ fuel active = extractAux κ fuel active

Two pairings which are full and primitive on every block of one concrete Definition 3.1 schedule execute the same endpoint selector recursion.

The exact R-322 endpoint fibre product

theorem Anderson4D.extract_eq_of_extractionPrimitivePartitionFiber {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (τ : PrimitivePartitionFiber (extractionPrimitiveBlockPartition κ hκ)) : extract ↑τ = extract κ

Every pairing which is full and primitive on the concrete extraction blocks of a full reference pairing has exactly the same ordered extraction list.

def Anderson4D.reductionEndpointFiberEquivPrimitivePartitionFiber {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) : ReductionEndpointFiberAt κ ≃ PrimitivePartitionFiber (extractionPrimitiveBlockPartition κ hκ)

Generic primitive-partition fibres for the concrete extraction schedule are exactly the complete endpoint-signature fibre.

Equations

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

noncomputable def Anderson4D.endpointFiberEquivPrimitiveCoordinates {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) : ReductionEndpointFiberAt κ ≃ ExtractionPrimitiveCoordinates κ

Exact multi-block product for an R-322 endpoint fibre. Every realized endpoint-signature fibre has one independent primitive full pairing coordinate on each concrete Definition 3.1 block, with no quotient, multiplicity, or cardinality factor.

Equations

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

theorem Anderson4D.endpointFiberEquivPrimitiveCoordinates_apply {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (τ : ReductionEndpointFiberAt κ) : (endpointFiberEquivPrimitiveCoordinates κ hκ) τ = endpointFiberPrimitiveCoordinates κ τ

The public product equivalence uses the previously frozen coordinate map on its forward direction.

theorem Anderson4D.sum_endpointFiber_eq_sum_primitiveCoordinates {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) {M : Type u_1} [AddCommMonoid M] (F : ReductionEndpointFiberAt κ → M) : ∑ τ : ReductionEndpointFiberAt κ, F τ = ∑ coordinates : ExtractionPrimitiveCoordinates κ, F ((endpointFiberEquivPrimitiveCoordinates κ hκ).symm coordinates)

Exact finite-sum reindexing of an endpoint fibre by all primitive block coordinates.