Masses Mass Genesis T10 Shape Selector Raw Canonical Positive Stationary Mode Of

The raw mode bridge

The declaration rawCanonicalPositiveStationaryMode_of_t10SourceData is a theorem in the framework's machine-checked library of formal theorems. It states a conditional result: if a light pattern ψ satisfies a structure called T10RawModeSourceData, then that pattern is an instance of a raw canonical positive stationary primitive factor mode. In plainer words, the theorem says that when certain specified conditions about a pattern's support, neutrality, and amplitude are met, the pattern qualifies as a particular stable, fundamental matter mode. The proof is a formal derivation: it takes the three components of the source data and assembles them, using an existing theorem about how neutral components combine, to conclude the mode property.

The content of T10RawModeSourceData is the heart of the matter. It packages three obligations. First, anchor_neutral asserts that the pattern's anchor phase is neutral. Second, phase0_amplitude fixes the amplitude at phase zero. Third, and most importantly, anchor_support_of_post is a function that takes a legal first Gray-edge posting and returns a proof that the anchor has the required support. This third item is the explicit, still-open bridge: the theorem does not prove that a legal posting implies the support condition. It only states that if such an implication is supplied, then the mode follows. The docstring is explicit that bare one-bit posting does not itself prove the support statement.

What the theorem does not claim is as important as what it proves. It does not derive the matter window from the ledger. The missing physical bridge must identify ledger parity with the Q3 clock vertices and identify the two posted states with the occupied phases of the raw photon window. The theorem takes these identifications as inputs, not as consequences. It also does not claim that the fixed Gray clock is the only possible clock: a separate theorem in the same file proves that a legal atomic post can escape the Gray clock, meaning legality and one-bit parity alone cannot derive next-clock settlement. The theorem is a bridge over a gap, not the gap itself.

The practical upshot is a precise accounting of what is known and what remains open in this corner of the framework. The local cube discriminator and its Gray-clock obstruction are proved. The raw mode follows from a named ledger/window realization interface. But physical stability supplies the nine-row charged image without choosing a unique topology, so a species or topology label is still required before fixed-topology pattern rigidity can be used. The theorem names its obligations without treating them as proved.

/-- The named source boundary is sufficient for the raw canonical mode. The
proof uses the explicit, still-open `anchor_support_of_post` bridge and uses
neutrality to derive the opposite phase-one amplitude. Bare one-bit posting
does not itself prove the support statement. -/
theorem rawCanonicalPositiveStationaryMode_of_t10SourceData
    (ψ : LightPattern (Fin 8))
    (h : T10RawModeSourceData ψ) :
    AnchorPhaseRawCanonicalPositiveStationaryPrimitiveFactorMode ψ := by
  apply rawCanonicalPositiveStationaryMode_of_components
  exact rawCanonicalComponents_of_neutralComponents ψ
    { anchor_neutral := h.anchor_neutral
      phase0_amplitude := h.phase0_amplitude
      tail_zero := h.anchor_support_of_post h.first_edge_post }

/-- The exact source data still needed to carry a legal first Gray-edge post
into the raw canonical positive-stationary matter mode.

`anchor_support_of_post` is the missing ledger-to-photon support bridge.
`anchor_neutral` and `phase0_amplitude` are independent raw-window facts; they
are not consequences of one-bit parity adjacency alone. -/
structure T10RawModeSourceData (ψ : LightPattern (Fin 8)) where
  source_ledger : LedgerState 3
  target_ledger : LedgerState 3
  first_edge_post :
    Q3PostingRealization source_ledger target_ledger 0 1
  anchor_support_of_post :
    Q3PostingRealization source_ledger target_ledger 0 1 →
      ∀ i : Fin 8, i.val ≠ 0 → i.val ≠ 1 → ψ.window 0 i = 0
  anchor_neutral :
    IsNeutral (ψ.window 0)
  phase0_amplitude :
    ψ.window 0 0 =
      (primitivePositiveStationaryFactorAmplitude ψ : ℂ)

/-- **Posting-to-clock wall.** A legal atomic post can traverse a one-bit cube
edge omitted by the fixed Gray clock. Therefore legality and one-bit parity
alone cannot derive next-clock settlement or photon gap-one support. -/
theorem legalAtomicTick_can_escape_grayClock :
    ∃ L L' : LedgerState 3,
      LegalAtomicTick (d := 3) L L' ∧
      ¬ GrayClockEdge (parity 3 L) (parity 3 L') := by
  rcases jMinimalPosting_can_escape_grayClock with
    ⟨L, L', hmin, _hL, _hL', hnot⟩
  refine ⟨L, L', ?_, hnot⟩
  exact postingStep_implies_legalAtomicTick
    (minJlogCost_monotoneStep_implies_postingStep
      hmin.1 hmin.2.1 hmin.2.2)

/-- The existing physical-stability predicate therefore admits distinct
charged topologies. It selects the exact nine-row charged image, not one
topology, so a species/topology label is still required before fixed-topology
pattern rigidity can be used. -/
theorem physicallyStableCharged_topology_not_unique :
    ∃ T U : PatternTopology,
      PhysicallyStableCharged T ∧
      PhysicallyStableCharged U ∧
      T ≠ U :=
  exactChargedTopologyImage_not_singleton physicalStability_charged_image

What this page does not claim

The theorem does not prove that the matter window is derived from the ledger alone. The theorem does not show that the fixed Gray clock is the only possible clock for legal postings. The theorem does not establish uniqueness of the raw mode without a fixed topology label.

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/T10ShapeSelector.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: