Encyclopedia Masses Masses Mass Genesis Anchor Sector Transport
ARTICLE 3 claims 3 theorems
Masses Mass Genesis Anchor Sector Transport
Mass Genesis splits one amplitude into a base chord and a scaling step, and the split is a theorem, not a new assumption.
The transport split
In the Recognition Science framework, particle masses are not fitted values but outcomes of a forced chain of structure. The framework's machine-checked library of formal theorems builds this chain from a single cost function, and the Mass Genesis module is where that chain reaches the particle spectrum. Its task is to turn a single complex amplitude, a number that encodes a particle's phase behavior, into a form that separates what a particle is from how it scales.
The module defines anchor sector transport, a two-part decomposition of that amplitude. The first part is a sector-base chord: a neutral unit vector scaled only by the sector amplitude, the part of the signal that carries the particle's identity. The second part is phi transport, a scaling step selected by the particle's rung and charge that stretches that base chord into the actual phase-0 neutral window. The key fact is that this split is theorem-equivalent to the original single amplitude target. Nothing is added or lost; the module proves that the two-part form and the one-part form describe the same object.
Why split at all? The framework's goal is to derive each piece from a deeper principle. The sector-base chord should eventually be proven from Q3 topology, the three-dimensional linking structure that the framework forces. The phi transport step should be proven from the golden-ratio scaling law and the rung and charge dynamics. The split gives each derivation a clean target. It is an interface, not a new physical claim.
The module also proves limits on what the structure alone can force. A pattern can have full eight-tick support and still fail to have an equivariant window, and a stable closed light pattern can fail to occupy the anchor pair. These are not failures; they are boundary markers. They show that the transport split is doing real work, because the surrounding conditions do not automatically guarantee it.
What the split changes is the shape of the remaining proof obligation. Instead of one opaque amplitude, the framework now has two concrete targets, each with a named mechanism that should produce it. The transport split is the hinge that lets the mass spectrum hang from the forcing chain.
THEOREM anchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
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 fullSupport_does_not_force_windowEquivariant · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
/-- **OBSTRUCTION (carrier dynamics, O3 residue).** Full eight-tick support does NOT
force `EightTickWindowEquivariant`. The constant pattern on the gap-1 neutral window has
full support but fails window-equivariance, because the gap-1 window is not R̂-fixed
(`cyclicShift` moves its phase-0 entry from `1` to `-1`). So window-equivariance is
genuine dynamical data independent of the Q3/R̂ support topology — the worldline
identification of site-step with R̂-tick, not a consequence of full support. -/
theorem fullSupport_does_not_force_windowEquivariant :
FullEightTickSupport (constWindowPattern gapOneTwoPhaseMode) ∧
¬ EightTickWindowEquivariant (constWindowPattern gapOneTwoPhaseMode) := by
refine ⟨rfl, ?_⟩
intro hequiv
have h := hequiv 0
simp only [constWindowPattern, eightTickSupportStep] at h
have h0 := congrFun h 0
have hcs : RecognitionDynamics.cyclicShift gapOneTwoPhaseMode 0
= gapOneTwoPhaseMode 1 := by
simp only [RecognitionDynamics.cyclicShift]; congr 1
rw [hcs] at h0
simp only [gapOneTwoPhaseMode] at h0
norm_num at h0
THEOREM stableClosed_does_not_force_anchorOccupied · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
/-- **OBSTRUCTION (carrier dynamics, O2 residue).** The full dynamical stable
predicate — localization, nontrivial neutral load, and a closed eight-tick R̂
orbit — does NOT force anchor occupancy. The raw counterexample is a proven
`StableClosedLightPattern` (left conjunct) whose anchor phase 0 is empty (right
conjunct). Since `R̂ = cyclicShift` (`ClosedRHatOrbit` is stated with `cyclicShift`,
and `cyclicShift ψ t = ψ (t+1)`), the occupied phase index is the basepoint-free
R̂-orbit coordinate, not an R̂-invariant. Anchor occupancy is therefore a choice of
orbit basepoint (frame); the stable predicate alone cannot supply it. -/
theorem stableClosed_does_not_force_anchorOccupied :
StableClosedLightPattern rawTailStableCounterexample
∧ ¬ AnchorPairOccupied rawTailStableCounterexample :=
⟨rawTailStableCounterexample_stable,
rawTailStableCounterexample_not_anchorOccupied⟩
What this page does not claim
No claim that the sector-base chord or phi transport step has been derived from Q3 topology or phi forcing. No claim that any particle mass has been computed from this module. No claim that the transport split is physically observable rather than a formal decomposition.
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:
- How does Q3 topology prove the sector-base chord?
- What rung and charge dynamics select the phi transport scaling?
- Which measured particle masses does the transport split reproduce?
- What is the phase-0 neutral window in physical terms?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM anchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
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.The split is theorem-equivalent to the previous CP6 amplitude target. anchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.leanTHEOREM fullSupport_does_not_force_windowEquivariant · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
/-- **OBSTRUCTION (carrier dynamics, O3 residue).** Full eight-tick support does NOT force `EightTickWindowEquivariant`. The constant pattern on the gap-1 neutral window has full support but fails window-equivariance, because the gap-1 window is not R̂-fixed (`cyclicShift` moves its phase-0 entry from `1` to `-1`). So window-equivariance is genuine dynamical data independent of the Q3/R̂ support topology — the worldline identification of site-step with R̂-tick, not a consequence of full support. -/ theorem fullSupport_does_not_force_windowEquivariant : FullEightTickSupport (constWindowPattern gapOneTwoPhaseMode) ∧ ¬ EightTickWindowEquivariant (constWindowPattern gapOneTwoPhaseMode) := by refine ⟨rfl, ?_⟩ intro hequiv have h := hequiv 0 simp only [constWindowPattern, eightTickSupportStep] at h have h0 := congrFun h 0 have hcs : RecognitionDynamics.cyclicShift gapOneTwoPhaseMode 0 = gapOneTwoPhaseMode 1 := by simp only [RecognitionDynamics.cyclicShift]; congr 1 rw [hcs] at h0 simp only [gapOneTwoPhaseMode] at h0 norm_num at h0A pattern can have full eight-tick support and still fail to have an equivariant window. fullSupport_does_not_force_windowEquivariant · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.leanTHEOREM stableClosed_does_not_force_anchorOccupied · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
/-- **OBSTRUCTION (carrier dynamics, O2 residue).** The full dynamical stable predicate — localization, nontrivial neutral load, and a closed eight-tick R̂ orbit — does NOT force anchor occupancy. The raw counterexample is a proven `StableClosedLightPattern` (left conjunct) whose anchor phase 0 is empty (right conjunct). Since `R̂ = cyclicShift` (`ClosedRHatOrbit` is stated with `cyclicShift`, and `cyclicShift ψ t = ψ (t+1)`), the occupied phase index is the basepoint-free R̂-orbit coordinate, not an R̂-invariant. Anchor occupancy is therefore a choice of orbit basepoint (frame); the stable predicate alone cannot supply it. -/ theorem stableClosed_does_not_force_anchorOccupied : StableClosedLightPattern rawTailStableCounterexample ∧ ¬ AnchorPairOccupied rawTailStableCounterexample := ⟨rawTailStableCounterexample_stable, rawTailStableCounterexample_not_anchorOccupied⟩A stable closed light pattern can fail to occupy the anchor pair. stableClosed_does_not_force_anchorOccupied · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean