Encyclopedia Masses Masses Mass Genesis Anchor Sector Transport Tail Local Topology Sector Dyadic Ph
ARTICLE 3 claims 3 theorems
Masses Mass Genesis Anchor Sector Transport Tail Local Topology Sector Dyadic Ph
A machine-checked library shows how particle mass generation splits into a base pattern and a scaling step, without claiming the physical bridge is complete.
The transport split
In the Recognition Science framework, mass generation for particles is studied through recognition events, discrete records of how a system's states change. A central idea is that the process can be split into two parts: a fixed base pattern, called the sector-base chord, and a transport step that scales that pattern according to the particle's rung and charge. The declaration tailLocalTopologySectorDyadicPhiRungFieldChargeFieldRatioGaugeData_of_tailLocalTopologySectorDyadicPhiRungFieldChargeBranchRatioGaugeData is a formal bridge between these two descriptions.
What the declaration establishes, in plain terms, is that the split is theorem-equivalent to the previous single-amplitude target. If the base chord and the transport step are both present, the full amplitude follows; conversely, the full amplitude implies both parts. This is a cleaner interface for further work: one part of the proof can focus on the topology of the base chord, the other on the dynamics of the transport. The library proves this equivalence with machine-checked certainty, meaning no step is left to human judgment.
The framework also proves several limits on what these patterns can force. A pattern can have full support across all eight ticks without forcing the tail to vanish, and it can be stable and closed without forcing an anchor pair to be occupied. These results are important because they show that the transport split is not guaranteed by simple properties; it requires the specific structure of the amplitude.
What the declaration does not claim is that the physical bridge from recognition to linking is complete. The split is a formal step within the framework's mass genesis module. It does not, by itself, prove that the base chord arises from topology or that the transport step is forced by phi dynamics; those remain targets. It also does not claim that the split is unique or that it matches measured particle masses; that comparison is a separate empirical check.
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_tailVanishes · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
/-- **OBSTRUCTION (carrier dynamics, O1 residue).** Full eight-tick (site) support does NOT
force `AnchorPhaseTailVanishes`. The constant pattern on the gap-2 neutral window
(`gapTwoTwoPhaseMode`, load on phases 0 and 2) has full site support, yet its neutralized
phase-0 window has a nonzero entry at phase 2 (`neutralize gapTwoTwoPhaseMode 2 = -1`), so
the tail does not vanish. Tail exclusion is therefore a window-phase condition equivalent to
O2's two-phase support (`tailVanishes_iff_twoPhaseSupport`), not a consequence of the spatial
step-closure that discharges `FullEightTickSupport`. O1 inherits O2's conditional status. -/
theorem fullSupport_does_not_force_tailVanishes :
FullEightTickSupport (constWindowPattern gapTwoTwoPhaseMode) ∧
¬ AnchorPhaseTailVanishes (constWindowPattern gapTwoTwoPhaseMode) := by
refine ⟨rfl, ?_⟩
intro htail
have h := htail.phase2_zero
simp only [constWindowPattern] at h
have hval : neutralize gapTwoTwoPhaseMode (2 : Fin 8) = -1 := by
show gapTwoTwoPhaseMode 2 - (∑ i, gapTwoTwoPhaseMode i) / 8 = -1
rw [gapTwoTwoPhaseMode_neutral]
norm_num [gapTwoTwoPhaseMode]
rw [hval] at h
norm_num at h
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
The physical recognition-to-linking bridge is complete. The split is unique among possible decompositions. The transport step is forced by phi dynamics alone. The framework derives the fine-structure constant.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What specific topology proof would establish the sector-base chord?
- What phi dynamics would force the transport step for a given rung and charge?
- How does the transport split relate to the measured phi-power mass ladder?
- What is the physical interpretation of the anchor phase in recognition events?
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 single-amplitude target. anchorSectorTransportCert · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.leanTHEOREM fullSupport_does_not_force_tailVanishes · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
/-- **OBSTRUCTION (carrier dynamics, O1 residue).** Full eight-tick (site) support does NOT force `AnchorPhaseTailVanishes`. The constant pattern on the gap-2 neutral window (`gapTwoTwoPhaseMode`, load on phases 0 and 2) has full site support, yet its neutralized phase-0 window has a nonzero entry at phase 2 (`neutralize gapTwoTwoPhaseMode 2 = -1`), so the tail does not vanish. Tail exclusion is therefore a window-phase condition equivalent to O2's two-phase support (`tailVanishes_iff_twoPhaseSupport`), not a consequence of the spatial step-closure that discharges `FullEightTickSupport`. O1 inherits O2's conditional status. -/ theorem fullSupport_does_not_force_tailVanishes : FullEightTickSupport (constWindowPattern gapTwoTwoPhaseMode) ∧ ¬ AnchorPhaseTailVanishes (constWindowPattern gapTwoTwoPhaseMode) := by refine ⟨rfl, ?_⟩ intro htail have h := htail.phase2_zero simp only [constWindowPattern] at h have hval : neutralize gapTwoTwoPhaseMode (2 : Fin 8) = -1 := by show gapTwoTwoPhaseMode 2 - (∑ i, gapTwoTwoPhaseMode i) / 8 = -1 rw [gapTwoTwoPhaseMode_neutral] norm_num [gapTwoTwoPhaseMode] rw [hval] at h norm_num at hA pattern can have full support across all eight ticks without forcing the tail to vanish. fullSupport_does_not_force_tailVanishes · 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 pattern can be stable and closed without forcing an anchor pair to be occupied. stableClosed_does_not_force_anchorOccupied · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean