Encyclopedia Masses Masses Mass Genesis Anchor Sector Transport Tail Local Topology Sector Combined

ARTICLE 3 claims 1 theorem 2 models

Masses Mass Genesis Anchor Sector Transport Tail Local Topology Sector Combined

Mass generation in Recognition Science splits into two steps: a base sector chord and a phi-scaled transport, and the split is theorem-equivalent to the original single amplitude target.

Verify this page

The transport split

In the Recognition Science framework, mass generation is the problem of producing the observed particle masses from a discrete record of recognition events, called the ledger. The framework's library, a machine-checked collection of formal theorems, reduces this problem to a single amplitude realization at a specific phase, the anchor phase. The declaration in question establishes that this single target can be split into two distinct physical obligations without loss of mathematical content.

The first obligation is a sector-base neutral chord: a unit vector, scaled only by the sector amplitude, that carries the base geometry of the sector. The second is a phi transport step, selected by rung and charge, that scales this base chord into the actual phase-0 neutral window. The split is theorem-equivalent to the previous single CP6 amplitude target, meaning the two-step description and the one-step description are provably the same object in the framework.

This split is a cleaner bottom-up interface for further work. The framework's topology should prove the sector base chord, and the phi forcing, rung, and charge dynamics should prove the transport step. The declaration does not claim that either step is already proven; it establishes that the two-step formulation is equivalent to the prior target, not that the target is achieved.

The declaration also does not claim that the split is physically unique or that it resolves the mass problem. It is a structural reorganization, a way of dividing a known target into two more tractable pieces. The framework's own theorems show that several natural conditions, such as full support or stability, do not by themselves force the desired tail or phase properties, so the split is a starting point for proof, not a finished derivation.

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.
MODEL primitiveTopologySectorChargeNumerator · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
primitiveTopologySectorChargeNumerator · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean:1132 
/-- Charge numerator attached to the topology-derived sector branch. -/
def primitiveTopologySectorChargeNumerator
    (ψ : LightPattern (Fin 8)) : ℤ :=
  match primitiveTopologyBranchSector ψ with
  | Anchor.Sector.Electroweak => 0
  | Anchor.Sector.Lepton =>
      ψ.topology.chargeSkew ^ (2 : ℕ) +
        ψ.topology.chargeSkew ^ (4 : ℕ)
  | Anchor.Sector.UpQuark =>
      (ψ.topology.q3LoopRank : ℤ) +
        ψ.topology.chargeSkew ^ (2 : ℕ) +
        ψ.topology.chargeSkew ^ (4 : ℕ)
  | Anchor.Sector.DownQuark =>
      (ψ.topology.q3LoopRank : ℤ) +
        ψ.topology.chargeSkew ^ (2 : ℕ) +
        ψ.topology.chargeSkew ^ (4 : ℕ)
MODEL primitiveTopologyCombinedPhiBranchScalarLoad · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
primitiveTopologyCombinedPhiBranchScalarLoad · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean:1046 
/-- Fully branch-inline scalar with the sector and raw-rung phi factors combined
into a single topology exponent in each branch. -/
noncomputable def primitiveTopologyCombinedPhiBranchScalarLoad
    (ψ : LightPattern (Fin 8)) : ℝ :=
  let s := ((ψ.topology.spinClass + ψ.topology.generationTorsion +
    (ψ.topology.q3ActiveEdges : ℤ) : ℤ) : ℝ)
  if ψ.topology.chargeSkew = 0 then
    (2 : ℝ) ^ (-(3 : ℤ)) * Constants.phi ^ (s + 42)
  else if ψ.topology.q3LoopRank = 0 then
    ((2 : ℝ) ^ (-(26 : ℤ)) * Constants.phi ^ (s + 49)) *
      (1 + ((ψ.topology.chargeSkew ^ (2 : ℕ) +
        ψ.topology.chargeSkew ^ (4 : ℕ) : ℤ) : ℝ) / Constants.phi)
  else if 0 < ψ.topology.chargeSkew then
    ((2 : ℝ) ^ (-(5 : ℤ)) * Constants.phi ^ (s + 22)) *
      (1 + (((ψ.topology.q3LoopRank : ℤ) +
        ψ.topology.chargeSkew ^ (2 : ℕ) +
        ψ.topology.chargeSkew ^ (4 : ℕ) : ℤ) : ℝ) / Constants.phi)
  else
    ((2 : ℝ) ^ (19 : ℤ) * Constants.phi ^ (s - 18)) *
      (1 + (((ψ.topology.q3LoopRank : ℤ) +
        ψ.topology.chargeSkew ^ (2 : ℕ) +
        ψ.topology.chargeSkew ^ (4 : ℕ) : ℤ) : ℝ) / Constants.phi)

What this page does not claim

The declaration does not prove that either the sector base chord or the phi transport step is actually realized. The declaration does not claim the split is physically unique. The declaration does not resolve the mass generation problem; it reorganizes it.

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