Encyclopedia Masses Masses Mass Genesis Anchor Sector Transport Tail Local Topology Sector Field Run
ARTICLE 5 claims 5 theorems
Masses Mass Genesis Anchor Sector Transport Tail Local Topology Sector Field Run
Mass genesis in this framework splits into a fixed sector base and a transport step, and the split is proven equivalent to the original amplitude target.
The split theorem
In the Recognition Science framework, particle masses are built from a discrete record of eight phase positions, a ledger of events around a cycle. The framework's Mass Genesis module aims to reduce the whole mass story to a single amplitude at one anchor phase. The declaration in question, tailLocalTopologySectorFieldRungFieldChargeFieldRatioGaugeData_of_tailLocalTopologySectorConstantRungFieldChargeFieldRatioGaugeData, establishes that this single amplitude can be split into two separate physical obligations without changing the result.
The first obligation is a sector-base neutral chord: a unit vector scaled only by the sector amplitude, carrying the sector's identity. The second is a phi transport step, selected by rung and charge, which scales that base chord into the actual phase-0 neutral window. The split is theorem-equivalent to the previous CP6 amplitude target, meaning the two formulations are interchangeable within the framework's logic. This is a cleaner bottom-up interface: the Q3 topology should prove the sector base chord, and phi forcing with rung and charge dynamics should prove the transport step.
The framework also proves several limits on what such patterns can force. Full eight-tick support does not force the tail to vanish, nor does it force window equivariance. A stable closed light pattern does not force the anchor to be occupied, and minimal neutral support does not force a two-phase anchor. These results are part of the same module and clarify the boundaries of what the transport split can assume.
What the declaration does not claim is broader. It does not prove that the sector base chord or the transport step actually exist for any given pattern; it only proves the equivalence of the split formulation to the original target. The physical bridge from recognition to linking, which would justify the topology, remains open. The split is a structural reorganization, not a derivation of mass values from first principles.
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 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⟩
THEOREM minimalNeutralSupport_does_not_force_anchorTwoPhase · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
/-- **OBSTRUCTION (carrier dynamics, O2 residue).** Minimal neutral support does
NOT force anchor two-phase support. The raw counterexample has minimal neutral
support (left conjunct) — a single opposite-phase pair at `{2, 3}` — yet fails
`AnchorPhaseTwoPhaseSupport` (right conjunct) because its pair is not the anchor
pair `(0, 1)`. So the remaining content of O2 is exactly the anchor-pair
selection: deriving that the carrier's occupied pair is `(0, 1)`. That is a gauge
fact (CP6 / sector anchor, the O4 line), not a consequence of neutrality or
support-minimality. This factors O2 into a solved structural part (one
antisymmetric pair) and a single open gauge part (the pair is the anchor pair). -/
theorem minimalNeutralSupport_does_not_force_anchorTwoPhase :
MinimalNeutralSupport rawTailStableCounterexample
∧ ¬ AnchorPhaseTwoPhaseSupport rawTailStableCounterexample :=
⟨rawTailStableCounterexample_minimalNeutralSupport,
rawTailStableCounterexample_not_twoPhaseSupport⟩
What this page does not claim
The declaration does not prove that the sector base chord or transport step exist for any given pattern. The physical recognition-to-linking bridge remains open. The split does not derive specific mass values from first principles.
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 physical mechanism selects the sector base chord from Q3 topology?
- How do rung and charge dynamics determine the phi transport step?
- What would a counterexample to the split equivalence look like?
- Does the transport split generalize to patterns with more than eight ticks?
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_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 hFull eight-tick support does not force the tail to vanish. fullSupport_does_not_force_tailVanishes · 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 h0Full eight-tick support does not force window equivariance. 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 does not force the anchor to be occupied. stableClosed_does_not_force_anchorOccupied · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.leanTHEOREM minimalNeutralSupport_does_not_force_anchorTwoPhase · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean
/-- **OBSTRUCTION (carrier dynamics, O2 residue).** Minimal neutral support does NOT force anchor two-phase support. The raw counterexample has minimal neutral support (left conjunct) — a single opposite-phase pair at `{2, 3}` — yet fails `AnchorPhaseTwoPhaseSupport` (right conjunct) because its pair is not the anchor pair `(0, 1)`. So the remaining content of O2 is exactly the anchor-pair selection: deriving that the carrier's occupied pair is `(0, 1)`. That is a gauge fact (CP6 / sector anchor, the O4 line), not a consequence of neutrality or support-minimality. This factors O2 into a solved structural part (one antisymmetric pair) and a single open gauge part (the pair is the anchor pair). -/ theorem minimalNeutralSupport_does_not_force_anchorTwoPhase : MinimalNeutralSupport rawTailStableCounterexample ∧ ¬ AnchorPhaseTwoPhaseSupport rawTailStableCounterexample := ⟨rawTailStableCounterexample_minimalNeutralSupport, rawTailStableCounterexample_not_twoPhaseSupport⟩Minimal neutral support does not force a two-phase anchor. minimalNeutralSupport_does_not_force_anchorTwoPhase · IndisputableMonolith/Masses/MassGenesis/AnchorSectorTransport.lean