Masses Mass Genesis T10 Settlement Readout Image Gate T10 Settlement Readout Ima

The readout gate

The declaration t10SettlementReadoutImageGateCert is a machine-checked certificate, a formal proof object in the framework's library of verified theorems. It establishes a precise negative result about the readout process in the mass-genesis construction. In plain language, it proves that when a settled octave, a completed eight-tick recognition cycle, is measured by any local settlement readout, the resulting image always falls into a specific classification class, the gap-one class. The certificate simultaneously proves that this image can never fall into the neighboring gap-two class.

The two theorems that constitute the certificate work together. The first, localSettlementReadout_image_rhatClass_eq_gapOne, shows that the readout of any settled octave, at any of the eight phases, lands in the gap-one class. The second, localSettlementReadout_image_rhatClass_ne_gapTwo, shows the same readout is never in the gap-two class. Together they establish a clean discrimination boundary: the readout of a settled octave is always gap-one, never gap-two. This is the negative half of an admission gate for readout parents, meaning it rules out a specific class of physical photon countermodels from being realized by settled octaves.

The certificate's power lies in its scope and its limits. It proves a property of all local settlement readouts applied to all settled octaves, for every phase. It does not, however, prove that any particular physical state, such as PhysicalPhotonState.window, belongs to the readout image. The certificate establishes where the readout images land, not which specific physical states are realized. It is a constraint on the possible, not an assertion of the actual.

In the framework's account, this certificate is a load-bearing piece of the mass-genesis story. It shows that the settled octave structure is stable against a certain class of readout ambiguity: no settled octave can masquerade as the gap-two countermodel. This is what the framework means by a discrimination test being frozen. The certificate does not derive the physical bridge from recognition to measurement; that remains an open target. It secures one boundary of that bridge, proving that whatever crosses it from a settled octave carries the gap-one signature.

theorem t10SettlementReadoutImageGateCert :
    T10SettlementReadoutImageGateCert where
  image_is_gap_one := localSettlementReadout_image_rhatClass_eq_gapOne
  gap_two_excluded := localSettlementReadout_image_rhatClass_ne_gapTwo

/-- Every local settlement readout of a settled octave lies in the gap-one
Rhat class. -/
theorem localSettlementReadout_image_rhatClass_eq_gapOne
    (octave : Q3SettledLedgerOctave)
    (L : LocalSettlementReadout)
    (phase : Fin 8) :
    Quotient.mk rhatOrbitSetoid
        (fun t =>
          L.amplitude (ledgerOccupationWindow octave phase t)
            (ledgerOccupationWindow octave phase (t - 1))) =
      Quotient.mk rhatOrbitSetoid gapOneTwoPhaseMode := by
  rw [settledLedger_settlement_law]
  exact commitSettlementWindow_rhatClass_eq_gapOne phase

/-- The gap-two countermodel is outside the image of every local settlement
readout on every settled octave. -/
theorem localSettlementReadout_image_rhatClass_ne_gapTwo
    (octave : Q3SettledLedgerOctave)
    (L : LocalSettlementReadout)
    (phase : Fin 8) :
    Quotient.mk rhatOrbitSetoid
        (fun t =>
          L.amplitude (ledgerOccupationWindow octave phase t)
            (ledgerOccupationWindow octave phase (t - 1))) ≠
      Quotient.mk rhatOrbitSetoid gapTwoTwoPhaseMode := by
  rw [settledLedger_settlement_law]
  exact commitSettlementWindow_rhatClass_ne_gapTwo phase

What this page does not claim

The certificate does not prove that PhysicalPhotonState.window belongs to the readout image. The certificate does not derive the physical recognition-to-linking bridge, which remains an open target. The certificate does not establish that any particular physical state is realized, only where readout images land.

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