Encyclopedia Masses Masses Mass Genesis Anchor Sector Transport Local Topology Sector Dyadic Phi Run
Masses Mass Genesis Anchor Sector Transport Local Topology Sector Dyadic Phi Run
A machine-checked library proves that two different ways of describing a particle's charge and scale are the same statement, not two separate assumptions.
The sector base and its transport
The declaration is an equivalence: it says that two descriptions of the same physical situation are interchangeable. One description starts from a field's charge and its ratio of branch magnitudes. The other starts from a branch ratio and derives the same charge. The theorem proves these two starting points are logically identical, so any result proved from one description transfers to the other.
In the Recognition Science framework, mass genesis is modeled as a discrete record of events, called a ledger. The framework's library, a machine-checked collection of formal theorems, contains this equivalence as a proved statement. The declaration is part of a larger module that splits the origin of mass into two obligations: a sector-base neutral chord, and a transport step that scales that chord by phi, the golden ratio, depending on rung and charge.
The equivalence matters because it gives a cleaner interface. One side of the equivalence, the field charge ratio, is what the topology of the eight-tick cycle should prove. The other side, the branch ratio, is what the phi forcing dynamics should prove. The theorem says these two proofs would be the same proof. It does not supply either proof. It establishes that the two descriptions are equivalent, not that either description is physically realized.
The declaration does not claim that the sector base chord exists, that phi transport happens, or that any particular particle mass is produced. It only claims that two formal descriptions are interchangeable. The counterexamples in the same module show that other properties, such as full support or stability, do not force the stronger conditions of anchor occupancy or two-phase support. Those are separate theorems with separate limits.
THEOREM AnchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
structure AnchorSectorTransportCert where
canonical_sector_base :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseSectorBaseCP6 ψ (canonicalSectorBaseVector ψ)
canonical_sector_base_norm :
∀ ψ : LightPattern (Fin 8),
normSq8 (canonicalSectorBaseVector ψ) =
primitiveAnchorSectorLoad ψ
rung_transport_amplitude_pos :
∀ ψ : LightPattern (Fin 8),
0 < primitiveRungTransportAmplitude ψ
charge_skew_transport_amplitude_pos :
∀ ψ : LightPattern (Fin 8),
0 < primitiveChargeSkewTransportAmplitude ψ
charge_skew_ratio_amplitude_pos :
∀ ψ : LightPattern (Fin 8),
0 < primitiveChargeSkewRatioAmplitude ψ
charge_skew_transport_amplitude_eq_ratio_amplitude :
∀ ψ : LightPattern (Fin 8),
primitiveChargeSkewTransportAmplitude ψ =
primitiveChargeSkewRatioAmplitude ψ
phi_transport_amplitude_splits :
∀ ψ : LightPattern (Fin 8),
primitivePhiTransportAmplitude ψ =
primitiveRungTransportAmplitude ψ *
primitiveChargeSkewTransportAmplitude ψ
sector_base_norm :
∀ (ψ : LightPattern (Fin 8)) {base : Fin 8 → ℂ},
AnchorPhaseSectorBaseCP6 ψ base →
normSq8 base = primitiveAnchorSectorLoad ψ
phi_transport_norm :
∀ (ψ : LightPattern (Fin 8)) {base : Fin 8 → ℂ},
AnchorPhasePhiTransport ψ base →
normSq8 base = primitiveAnchorSectorLoad ψ →
normSq8 (neutralize (ψ.window 0)) =
primitiveAnchorSectorLoad ψ * primitivePhiTransport ψ
sector_transport_iff_primitive_amplitude_cp6 :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseSectorTransportCP6 ψ ↔
AnchorPhasePrimitiveAmplitudeCP6 ψ
sector_transport_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3SectorTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
canonical_phi_transport_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalPhiTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
closed_amplitude_window_from_canonical_phi_transport :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseCanonicalPhiTransport ψ →
AnchorPhaseCanonicalClosedAmplitudeWindowData ψ
canonical_phi_transport_closes_via_closed_amplitude_window :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalPhiTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
canonical_phi_transport_from_rung_charge :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseCanonicalRungChargeTransport ψ →
AnchorPhaseCanonicalPhiTransport ψ
rung_charge_transport_from_ratio_transport :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseCanonicalRungChargeRatioTransport ψ →
AnchorPhaseCanonicalRungChargeTransport ψ
rung_charge_transport_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalRungChargeTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
rung_charge_transport_closes_via_closed_amplitude_window :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalRungChargeTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
rung_charge_ratio_transport_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalRungChargeRatioTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
rung_charge_ratio_transport_closes_via_closed_amplitude_window :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalRungChargeRatioTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
canonical_transport_iff_coordinates :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseCanonicalPhiTransport ψ ↔
AnchorPhaseCanonicalTransportCoordinates ψ
coordinate_transport_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalCoordinateTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
coordinate_transport_iff_components :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseCanonicalTransportCoordinates ψ ↔
AnchorPhaseCanonicalTransportComponents ψ
closed_amplitude_window_from_coordinates :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseCanonicalTransportCoordinates ψ →
AnchorPhaseCanonicalClosedAmplitudeWindowData ψ
component_transport_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalComponentTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
coordinate_transport_closes_via_closed_amplitude_window :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalCoordinateTransportMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
component_transport_iff_pair_data :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseCanonicalTransportComponents ψ ↔
AnchorPhaseCanonicalPairData ψ
pair_data_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalPairDataMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
antisymmetry_from_two_phase_support :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseTwoPhaseSupport ψ →
AnchorPhaseAnchorAntisymmetry ψ
support_amplitude_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalSupportAmplitudeMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
positive_magnitude_from_support_and_norm :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseTwoPhaseSupport ψ →
AnchorPhasePrimitiveAmplitudeNorm ψ →
AnchorPhasePositiveMagnitude ψ
positive_amplitude_from_magnitude_orientation :
∀ ψ : LightPattern (Fin 8),
AnchorPhasePositiveMagnitude ψ →
AnchorPhasePositivePhaseOrientation ψ →
AnchorPhasePositiveTransportAmplitude ψ
support_norm_orientation_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalSupportNormOrientationMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
support_factor_orientation_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalSupportFactorOrientationMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
positive_orientation_from_real_nonnegative :
∀ ψ : LightPattern (Fin 8),
AnchorPhase0Real ψ →
AnchorPhase0Nonnegative ψ →
AnchorPhasePositivePhaseOrientation ψ
support_factor_sign_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalSupportFactorSignMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
support_factor_gauge_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalSupportFactorGaugeMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
tail_vanishes_iff_two_phase_support :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseTailVanishes ψ ↔ AnchorPhaseTwoPhaseSupport ψ
tail_factor_gauge_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalTailFactorGaugeMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMass ψ = predictedMass ψ ∧
T.readout.inertialMass ψ = restMass ψ ∧
T.readout.gravitationalMass ψ = restMass ψ
factor_norm_iff_local_factor_magnitude_from_tail :
∀ ψ : LightPattern (Fin 8),
AnchorPhaseTailVanishes ψ →
(AnchorPhasePrimitiveFactorNorm ψ ↔
AnchorPhase0LocalFactorMagnitude ψ)
tail_local_gauge_closes_full_chain :
∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
Q3CanonicalTailLocalGaugeMassPatternEvidence ψ →
(∀ k : ℕ,
integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
0 < restMass ψ ∧
PhiRungQuantized ψ ∧
restMas
-- … truncated for the page; open the module for the rest.
What this page does not claim
The sector base chord exists in reality. Phi transport is physically realized. Any specific particle mass is derived from this equivalence alone.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What exactly is the sector-base neutral chord that the topology must prove?
- What is the phi transport step that the forcing dynamics must prove?
- Which particle masses, if any, follow from the sector base plus transport split?
- How does the eight-tick cycle topology prove the sector base chord?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM AnchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
structure AnchorSectorTransportCert where canonical_sector_base : ∀ ψ : LightPattern (Fin 8), AnchorPhaseSectorBaseCP6 ψ (canonicalSectorBaseVector ψ) canonical_sector_base_norm : ∀ ψ : LightPattern (Fin 8), normSq8 (canonicalSectorBaseVector ψ) = primitiveAnchorSectorLoad ψ rung_transport_amplitude_pos : ∀ ψ : LightPattern (Fin 8), 0 < primitiveRungTransportAmplitude ψ charge_skew_transport_amplitude_pos : ∀ ψ : LightPattern (Fin 8), 0 < primitiveChargeSkewTransportAmplitude ψ charge_skew_ratio_amplitude_pos : ∀ ψ : LightPattern (Fin 8), 0 < primitiveChargeSkewRatioAmplitude ψ charge_skew_transport_amplitude_eq_ratio_amplitude : ∀ ψ : LightPattern (Fin 8), primitiveChargeSkewTransportAmplitude ψ = primitiveChargeSkewRatioAmplitude ψ phi_transport_amplitude_splits : ∀ ψ : LightPattern (Fin 8), primitivePhiTransportAmplitude ψ = primitiveRungTransportAmplitude ψ * primitiveChargeSkewTransportAmplitude ψ sector_base_norm : ∀ (ψ : LightPattern (Fin 8)) {base : Fin 8 → ℂ}, AnchorPhaseSectorBaseCP6 ψ base → normSq8 base = primitiveAnchorSectorLoad ψ phi_transport_norm : ∀ (ψ : LightPattern (Fin 8)) {base : Fin 8 → ℂ}, AnchorPhasePhiTransport ψ base → normSq8 base = primitiveAnchorSectorLoad ψ → normSq8 (neutralize (ψ.window 0)) = primitiveAnchorSectorLoad ψ * primitivePhiTransport ψ sector_transport_iff_primitive_amplitude_cp6 : ∀ ψ : LightPattern (Fin 8), AnchorPhaseSectorTransportCP6 ψ ↔ AnchorPhasePrimitiveAmplitudeCP6 ψ sector_transport_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3SectorTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ canonical_phi_transport_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalPhiTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ closed_amplitude_window_from_canonical_phi_transport : ∀ ψ : LightPattern (Fin 8), AnchorPhaseCanonicalPhiTransport ψ → AnchorPhaseCanonicalClosedAmplitudeWindowData ψ canonical_phi_transport_closes_via_closed_amplitude_window : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalPhiTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ canonical_phi_transport_from_rung_charge : ∀ ψ : LightPattern (Fin 8), AnchorPhaseCanonicalRungChargeTransport ψ → AnchorPhaseCanonicalPhiTransport ψ rung_charge_transport_from_ratio_transport : ∀ ψ : LightPattern (Fin 8), AnchorPhaseCanonicalRungChargeRatioTransport ψ → AnchorPhaseCanonicalRungChargeTransport ψ rung_charge_transport_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalRungChargeTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ rung_charge_transport_closes_via_closed_amplitude_window : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalRungChargeTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ rung_charge_ratio_transport_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalRungChargeRatioTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ rung_charge_ratio_transport_closes_via_closed_amplitude_window : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalRungChargeRatioTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ canonical_transport_iff_coordinates : ∀ ψ : LightPattern (Fin 8), AnchorPhaseCanonicalPhiTransport ψ ↔ AnchorPhaseCanonicalTransportCoordinates ψ coordinate_transport_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalCoordinateTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ coordinate_transport_iff_components : ∀ ψ : LightPattern (Fin 8), AnchorPhaseCanonicalTransportCoordinates ψ ↔ AnchorPhaseCanonicalTransportComponents ψ closed_amplitude_window_from_coordinates : ∀ ψ : LightPattern (Fin 8), AnchorPhaseCanonicalTransportCoordinates ψ → AnchorPhaseCanonicalClosedAmplitudeWindowData ψ component_transport_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalComponentTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ coordinate_transport_closes_via_closed_amplitude_window : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalCoordinateTransportMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ component_transport_iff_pair_data : ∀ ψ : LightPattern (Fin 8), AnchorPhaseCanonicalTransportComponents ψ ↔ AnchorPhaseCanonicalPairData ψ pair_data_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalPairDataMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ antisymmetry_from_two_phase_support : ∀ ψ : LightPattern (Fin 8), AnchorPhaseTwoPhaseSupport ψ → AnchorPhaseAnchorAntisymmetry ψ support_amplitude_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalSupportAmplitudeMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ positive_magnitude_from_support_and_norm : ∀ ψ : LightPattern (Fin 8), AnchorPhaseTwoPhaseSupport ψ → AnchorPhasePrimitiveAmplitudeNorm ψ → AnchorPhasePositiveMagnitude ψ positive_amplitude_from_magnitude_orientation : ∀ ψ : LightPattern (Fin 8), AnchorPhasePositiveMagnitude ψ → AnchorPhasePositivePhaseOrientation ψ → AnchorPhasePositiveTransportAmplitude ψ support_norm_orientation_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalSupportNormOrientationMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ support_factor_orientation_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalSupportFactorOrientationMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ positive_orientation_from_real_nonnegative : ∀ ψ : LightPattern (Fin 8), AnchorPhase0Real ψ → AnchorPhase0Nonnegative ψ → AnchorPhasePositivePhaseOrientation ψ support_factor_sign_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalSupportFactorSignMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ support_factor_gauge_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalSupportFactorGaugeMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ tail_vanishes_iff_two_phase_support : ∀ ψ : LightPattern (Fin 8), AnchorPhaseTailVanishes ψ ↔ AnchorPhaseTwoPhaseSupport ψ tail_factor_gauge_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalTailFactorGaugeMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMass ψ = predictedMass ψ ∧ T.readout.inertialMass ψ = restMass ψ ∧ T.readout.gravitationalMass ψ = restMass ψ factor_norm_iff_local_factor_magnitude_from_tail : ∀ ψ : LightPattern (Fin 8), AnchorPhaseTailVanishes ψ → (AnchorPhasePrimitiveFactorNorm ψ ↔ AnchorPhase0LocalFactorMagnitude ψ) tail_local_gauge_closes_full_chain : ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)}, Q3CanonicalTailLocalGaugeMassPatternEvidence ψ → (∀ k : ℕ, integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧ 0 < restMass ψ ∧ PhiRungQuantized ψ ∧ restMas -- … truncated for the page; open the module for the rest.The theorem proves that two descriptions of the same physical situation are interchangeable. AnchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean