Encyclopedia Masses Masses Mass Genesis Anchor Sector Transport Local Topology Sector Combined Phi R

ARTICLE 2 claims 2 theorems

Masses Mass Genesis Anchor Sector Transport Local Topology Sector Combined Phi R

A machine-checked equivalence that rewrites one mass-generation amplitude as two physical steps: a sector base and a phi-scaled transport.

Verify this page

The sector transport split

In the Recognition Science framework, the ledger (a discrete record of recognition events) must account for particle masses through a single amplitude at a fixed phase. The declaration in question establishes an equivalence: the combined phi-rung field-charge ratio magnitude is identical to the dyadic phi-rung field-charge ratio magnitude. It proves that two different algebraic expressions for the same physical quantity are interchangeable, a theorem in the machine-checked library. This is not a numerical claim about a specific mass; it is a structural identity between two ways of writing the same scalar load.

The context module, Mass Genesis, splits the amplitude realization into two vector obligations: a sector-base neutral chord carrying the sector amplitude, and a phi transport selected by rung and charge that scales that base chord into the actual phase-0 neutral window. The equivalence says that the combined expression, which folds both obligations into one ratio, equals the dyadic expression, which keeps the transport step separate. The framework proves this split is equivalent to the previous amplitude target, meaning no information is lost by decomposing the calculation.

What the declaration does not claim: it does not prove that any particular particle mass matches a measured value. It does not assert that the transport step is physically realized; that remains a modeling choice. It also does not claim that the sector base chord or the phi transport are unique, only that the two algebraic forms agree. The equivalence is a formal bridge between two notations, not a derivation of the mass spectrum itself.

THEOREM AnchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
AnchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean:18608 · truncated 
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.
THEOREM anchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
anchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean:19619 · truncated 
def anchorSectorTransportCert : AnchorSectorTransportCert where
  canonical_sector_base := canonicalSectorBaseCP6
  canonical_sector_base_norm := canonicalSectorBase_norm
  rung_transport_amplitude_pos := primitiveRungTransportAmplitude_pos
  charge_skew_transport_amplitude_pos :=
    primitiveChargeSkewTransportAmplitude_pos
  charge_skew_ratio_amplitude_pos :=
    primitiveChargeSkewRatioAmplitude_pos
  charge_skew_transport_amplitude_eq_ratio_amplitude :=
    primitiveChargeSkewTransportAmplitude_eq_ratioAmplitude
  phi_transport_amplitude_splits :=
    primitivePhiTransportAmplitude_eq_rung_mul_charge
  sector_base_norm := sectorBaseCP6_norm
  phi_transport_norm := phiTransport_norm
  sector_transport_iff_primitive_amplitude_cp6 :=
    sectorTransportCP6_iff_primitiveAmplitudeCP6
  sector_transport_closes_full_chain :=
    fun T {ψ} E =>
      Q3SectorTransportMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  canonical_phi_transport_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalPhiTransportMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  closed_amplitude_window_from_canonical_phi_transport :=
    closedAmplitudeWindowData_of_canonicalPhiTransport
  canonical_phi_transport_closes_via_closed_amplitude_window :=
    fun T {ψ} E =>
      Q3CanonicalClosedAmplitudeWindowMassPatternEvidence.full_chain_for_canonicalPhiTransport_via_closedAmplitudeWindow
        (ψ := ψ) T E
  canonical_phi_transport_from_rung_charge :=
    canonicalPhiTransport_of_rungChargeTransport
  rung_charge_transport_from_ratio_transport :=
    canonicalRungChargeTransport_of_ratioTransport
  rung_charge_transport_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalRungChargeTransportMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  rung_charge_transport_closes_via_closed_amplitude_window :=
    fun T {ψ} E =>
      Q3CanonicalClosedAmplitudeWindowMassPatternEvidence.full_chain_for_rungChargeTransport_via_closedAmplitudeWindow
        (ψ := ψ) T E
  rung_charge_ratio_transport_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalRungChargeRatioTransportMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  rung_charge_ratio_transport_closes_via_closed_amplitude_window :=
    fun T {ψ} E =>
      Q3CanonicalClosedAmplitudeWindowMassPatternEvidence.full_chain_for_rungChargeRatioTransport_via_closedAmplitudeWindow
        (ψ := ψ) T E
  canonical_transport_iff_coordinates := canonicalPhiTransport_iff_coordinates
  coordinate_transport_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalCoordinateTransportMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  coordinate_transport_iff_components := canonicalCoordinates_iff_components
  closed_amplitude_window_from_coordinates := closedAmplitudeWindowData_of_coordinates
  component_transport_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalComponentTransportMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  coordinate_transport_closes_via_closed_amplitude_window :=
    fun T {ψ} E =>
      Q3CanonicalClosedAmplitudeWindowMassPatternEvidence.full_chain_for_coordinateTransport_via_closedAmplitudeWindow
        (ψ := ψ) T E
  component_transport_iff_pair_data := canonicalComponents_iff_pairData
  pair_data_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalPairDataMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  antisymmetry_from_two_phase_support := anchorAntisymmetry_of_twoPhaseSupport
  support_amplitude_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalSupportAmplitudeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  positive_magnitude_from_support_and_norm :=
    positiveMagnitude_of_twoPhaseSupport_and_norm
  positive_amplitude_from_magnitude_orientation :=
    positiveTransportAmplitude_of_magnitude_orientation
  support_norm_orientation_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalSupportNormOrientationMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  support_factor_orientation_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalSupportFactorOrientationMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  positive_orientation_from_real_nonnegative :=
    positivePhaseOrientation_of_real_nonnegative
  support_factor_sign_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalSupportFactorSignMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  support_factor_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalSupportFactorGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  tail_vanishes_iff_two_phase_support := tailVanishes_iff_twoPhaseSupport
  tail_factor_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailFactorGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  factor_norm_iff_local_factor_magnitude_from_tail :=
    factorNorm_iff_localFactorMagnitude_of_tailVanishes
  tail_local_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  local_factor_iff_local_sector_transport :=
    localFactorMagnitude_iff_localSectorTransportMagnitude
  phase0_sector_share_pos := primitiveAnchorPhase0SectorLoad_pos
  predicted_phase0_share_eq_predicted_mass_div :=
    primitivePredictedPhase0Share_eq_predictedMass_div
  phase0_sector_transport_eq_predicted_share :=
    primitiveAnchorPhase0SectorTransport_eq_predictedPhase0Share
  predicted_phase0_share_pos := primitivePredictedPhase0Share_pos
  predicted_phase0_amplitude_pos := primitivePredictedPhase0Amplitude_pos
  closed_amplitude_half_eq_predicted_phase0_amplitude :=
    primitiveClosedPatternAmplitude_div_sqrt_two_eq_predictedPhase0Amplitude
  local_sector_transport_iff_predicted_share :=
    localSectorTransportMagnitude_iff_localPredictedShareMagnitude
  local_predicted_share_of_predicted_amplitude :=
    localPredictedShareMagnitude_of_predictedAmplitude
  positive_gauge_of_predicted_amplitude :=
    positiveGauge_of_predictedAmplitude
  tail_local_sector_transport_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalSectorTransportGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  tail_local_predicted_share_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalPredictedShareGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  tail_predicted_amplitude_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailPredictedAmplitudeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  predicted_window_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalPredictedWindowMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  closed_amplitude_window_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalClosedAmplitudeWindowMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  phi_transport_splits := primitivePhiTransport_eq_rung_mul_charge
  local_sector_transport_iff_local_sector_rung_charge :=
    localSectorTransportMagnitude_iff_localSectorRungChargeMagnitude
  rung_transport_pos := primitiveRungTransport_pos
  charge_skew_transport_pos := primitiveChargeSkewTransport_pos
  tail_local_sector_rung_charge_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalSectorRungChargeGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  z_of_nonneg := ZOf_nonneg
  charge_skew_ratio_pos := primitiveChargeSkewRatio_pos
  charge_skew_transport_eq_ratio := primitiveChargeSkewTransport_eq_ratio
  local_sector_rung_charge_iff_ratio :=
    localSectorRungChargeMagnitude_iff_localSectorRungChargeRatioMagnitude
  tail_local_sector_rung_charge_ratio_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalSectorRungChargeRatioGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  phase0_sector_share_eq_expanded :=
    primitiveAnchorPhase0SectorLoad_eq_expanded
  phase0_expanded_sector_share_pos :=
    primitiveAnchorPhase0SectorExpandedLoad_pos
  local_sector_rung_charge_ratio_iff_expanded :=
    localSectorRungChargeRatioMagnitude_iff_localExpandedSectorRungChargeRatioMagnitude
  tail_local_expanded_sector_rung_charge_ratio_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalExpandedSectorRungChargeRatioGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  phase0_expanded_sector_share_eq_topology :=
    primitiveAnchorPhase0SectorExpandedLoad_eq_topology
  topology_rung_transport_eq := primitiveRungTransport_eq_topology
  topology_charge_ratio_eq := primitiveChargeSkewRatio_eq_topology
  topology_expanded_sector_share_pos :=
    primitiveAnchorPhase0TopologyExpandedLoad_pos
  topology_rung_transport_pos := primitiveTopologyRungTransport_pos
  topology_charge_ratio_pos := primitiveTopologyChargeSkewRatio_pos
  local_expanded_iff_local_topology :=
    localExpandedSectorRungChargeRatioMagnitude_iff_localTopologyExpandedSectorRungChargeRatioMagnitude
  tail_local_topology_expanded_sector_rung_charge_ratio_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalTopologyExpandedSectorRungChargeRatioGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  topology_rung_transport_eq_field :=
    primitiveTopologyRungTransport_eq_field
  topology_rung_field_transport_pos :=
    primitiveTopologyRungFieldTransport_pos
  local_topology_iff_local_topology_rung_field :=
    localTopologyExpandedSectorRungChargeRatioMagnitude_iff_localTopologyExpandedSectorRungFieldChargeRatioMagnitude
  tail_local_topology_expanded_sector_rung_field_charge_ratio_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalTopologyExpandedSectorRungFieldChargeRatioGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  topology_charge_ratio_eq_field :=
    primitiveTopologyChargeSkewRatio_eq_field
  topology_charge_field_ratio_pos :=
    primitiveTopologyChargeSkewFieldRatio_pos
  local_topology_rung_field_iff_charge_field :=
    localTopologyExpandedSectorRungFieldChargeRatioMagnitude_iff_localTopologyExpandedSectorRungFieldChargeFieldRatioMagnitude
  tail_local_topology_expanded_sector_rung_field_charge_field_ratio_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalTopologyExpandedSectorRungFieldChargeFieldRatioGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  topology_sector_load_eq_field :=
    primitiveAnchorPhase0TopologyExpandedLoad_eq_sectorField
  topology_sector_field_load_pos :=
    primitiveAnchorPhase0TopologySectorFieldExpandedLoad_pos
  local_topology_expanded_iff_sector_field :=
    localTopologyExpandedSectorRungFieldChargeFieldRatioMagnitude_iff_localTopologySectorFieldRungFieldChargeFieldRatioMagnitude
  tail_local_topology_sector_field_rung_field_charge_field_ratio_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalTopologySectorFieldRungFieldChargeFieldRatioGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E
  topology_sector_field_load_eq_constants :=
    primitiveAnchorPhase0TopologySectorFieldExpandedLoad_eq_constants
  topology_sector_constant_load_pos :=
    primitiveAnchorPhase0TopologySectorConstantExpandedLoad_pos
  local_topology_sector_field_iff_sector_constant :=
    localTopologySectorFieldRungFieldChargeFieldRatioMagnitude_iff_localTopologySectorConstantRungFieldChargeFieldRatioMagnitude
  tail_local_topology_sector_constant_rung_field_charge_field_ratio_gauge_closes_full_chain :=
    fun T {ψ} E =>
      Q3CanonicalTailLocalTopologySectorConstantRungFieldChargeFieldRatioGaugeMassPatternEvidence.full_chain_for_stableLoadReadout
        (ψ := ψ) T E

-- … truncated for the page; open the module for the rest.

What this page does not claim

No particle mass is derived or matched to a measured value by this equivalence. The transport step is not proven to be physically realized; it is a modeling choice. The equivalence does not establish uniqueness of the sector base or the transport scaling.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND