Encyclopedia Masses Masses Mass Genesis Anchor Sector Transport Tail Local Topology Sector Phi Rung

ARTICLE 2 claims 2 theorems

Masses Mass Genesis Anchor Sector Transport Tail Local Topology Sector Phi Rung

Mass Genesis splits one amplitude into a base chord and a transport step; the split is theorem-equivalent to the original target.

Verify this page

The transport split

In the Recognition Science framework, particle masses are built from a single primitive amplitude at a fixed anchor phase. The module AnchorSectorTransport reorganizes that amplitude into two distinct physical obligations: a sector-base neutral chord scaled by the sector amplitude, and a phi transport step selected by rung and charge that scales the base chord into the actual phase-0 neutral window.

This split is not an approximation or a heuristic. The framework's machine-checked library proves the split is theorem-equivalent to the previous CP6 amplitude target. The declaration tailLocalTopologySectorPhiRungFieldChargeFieldRatioGaugeData_of_tailLocalTopologySectorCombinedPhiRungFieldChargeFieldRatioGaugeData establishes that the combined phi-rung-field-charge-ratio gauge data implies the tail-local topology sector phi-rung-field-charge-ratio gauge data. In plain terms: if the combined data holds, then the local tail data necessarily holds as well. This is a logical implication, not a numerical equality.

The purpose of the split is architectural. The framework models the sector-base chord as the responsibility of Q3 topology, and the transport step as the responsibility of phi forcing, rung, and charge dynamics. The split provides a cleaner bottom-up interface: one part of the framework should prove the base chord, another should prove the transport step, and the theorem guarantees that proving both is equivalent to proving the original single amplitude.

What the declaration does not claim is equally important. It does not assert that any particular particle mass exists, that the transport step is physically realized, or that the split itself is unique. It does not claim that the tail-local data is sufficient for the combined data; only the reverse implication is established. The theorem is a structural bridge between two formulations of the same amplitude, not a physical prediction.

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.
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

The declaration does not assert that any specific particle mass exists. The declaration does not claim the tail-local data is sufficient for the combined data. The declaration does not claim the split is unique or physically realized.

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