Masses Mass Genesis T10 Settled Readout Decision Settled Readout Of Settled Boun

The settled readout

In the Recognition Science framework, matter is described through patterns and photons, where a ledger (a discrete record of events) tracks recognition events. A central question is whether the physical photon readout, the window of energy a photon carries, is identical to the settled anchor window of the pattern it reads. The declaration settledReadout_of_settledBoundary is a theorem that establishes this identity, but only under a specific, named condition.

The theorem states: if a model is a SettledCurrentPhysicalBoundaryModel3, meaning it already carries the assumption that the boundary is settled, then the photon window is the settled anchor. This is a conditional statement, not an unconditional derivation. The proof is a direct application of the carried field, PhotonWindowIsSettledAnchor.ofSettledBoundary. In plain terms, it says: if you assume the boundary is settled, then the readout matches. It does not, by itself, prove that any physical boundary is settled.

The framework is explicit about this limitation. A separate theorem, settledReadout_underdetermined_by_currentBoundary, proves that the current physical boundary data do not force the settled shape. There is a gap-two countermodel, settledReadout_gapTwo_countermodel, showing a model that is physical-photon compatible but does not have a settled anchor. This means the identification is not derived from first principles; it is a carried premise, a Branch C decision in the forced-matter closure. The full interface, ForcedMatterInterface3, includes this carried readout identification plus the sigma-zero constraint, and only then do theorems like restMass_eq_predictedMass and absolute_size follow.

What this declaration establishes is a precise, conditional bridge: within the framework, if the settled boundary is given, the readout is settled. What it does not claim is that this settled boundary is itself forced by more basic physics. That derivation remains outside the closed claim, a wall the framework acknowledges. The theorem is a piece of the larger mass-genesis story, but it is a piece that rests on a named assumption, not a free-standing result.

/-- On the settled boundary interface the photon window IS the settled
anchor (by the carried field). -/
theorem settledReadout_of_settledBoundary
    (model : SettledCurrentPhysicalBoundaryModel3) :
    PhotonWindowIsSettledAnchor
      model.base.photon model.base.pattern :=
  PhotonWindowIsSettledAnchor.ofSettledBoundary model

/-- Current physical boundary data underdetermine settlement shape. -/
theorem settledReadout_underdetermined_by_currentBoundary :
    ¬ ∀ model : PhasePostingPhysicalPhotonQ3Model3,
      PhotonWindowIsSettledAnchor model.photon model.pattern :=
  currentPhysicalBoundary_does_not_force_settledAnchorWindow

/-- Explicit gap-two countermodel: Q3 carrier, physical-photon compatible,
photon reads pattern anchor, yet not a settled anchor. -/
theorem settledReadout_gapTwo_countermodel :
    ∃ model : PhasePostingPhysicalPhotonQ3Model3,
      ¬ PhotonWindowIsSettledAnchor model.photon model.pattern :=
  exists_physicalBoundary_not_settledAnchor

What this page does not claim

The settled boundary is not derived from first principles by this declaration. The theorem does not prove that any physical boundary is settled. The identification is not claimed to be independent of the carried SettledAnchorWindow field.

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