Masses Mass Genesis T10 Genesis Orbit Selection Wall

The selection wall

In the Recognition Science framework, recognition (a discrete event of a system registering a state) carries a forced cost (a number measuring the price of that registration). The framework's library, a machine-checked collection of formal theorems, contains a result called the genesis orbit selection wall. It answers a precise question: among all possible rules that select the ground point of a certain scale orbit, the one that sets the recognition cost to zero is the only rule that works. The wall proves this classification for every such rule, regardless of how it is written or what constants it uses.

The setting is a one-dimensional scale orbit, a sequence of scales generated from a seed worldline pattern. Along this orbit, the framework's cost function J(x) = (x + 1/x)/2 - 1 vanishes at exactly one positive scale, called the factor amplitude f. The theorem genesisSelection_iff_sigmaZero_on_orbit states that any predicate satisfying the gate GenesisSelectsJGround (accept f, reject its double 2f, and pin at most one positive scale) is pointwise equivalent to the predicate that sets the cost to zero. A second theorem, genesisSelection_determined_on_orbit, sharpens this: any such selection predicate is equivalent to the simple equation s = f. The wall thus forces the selection content, no matter the costume the rule wears.

Two natural costumes are exhibited. The first, sigmaZeroOrbitPredicate, directly defines selection as the cost being zero. The second, massLawCostumePredicate, defines selection as the scale whose square equals the predicted mass divided by sixteen. The theorem massCostume_iff_sigmaZero_on_orbit proves these two are the same predicate at every positive orbit point. The link to mass comes from factorAmplitude_sq_eq_predictedMass_div_sixteen, which shows f² equals the predicted mass over sixteen, tying the abstract cost-zero point to a physical mass scale.

The wall's strength is its universality. It quantifies over all predicates from the real numbers to propositions, with no restriction on provenance. Any genesis-creation rule that selects the ground point is, on the orbit, the sigma-zero predicate. This closes the genesis side of a missing map, complementing a selector-side wall that ruled out certain field-to-current laws. The classification is complete at the predicate level, and the two sides name one object.

What this changes: the framework now knows that mass genesis, if it happens, cannot hide its selection rule. Any candidate rule that picks the ground state is forced to be the cost-zero rule, up to pointwise equivalence. The wall does not derive the value of f from deeper principles; that derivation remains open. But it pins down the structural form of any successful genesis rule, which is a necessary step toward a full theory of mass.

/-- **The genesis-orbit selection wall (THEOREM).** Every genesis-creation
predicate passing the gate is, at every positive scale of the orbit, the
σ-zero predicate `loadRecognitionCost = 0`. -/
theorem genesisSelection_iff_sigmaZero_on_orbit {P : ℝ → Prop}
    (hsel : GenesisSelectsJGround P) {s : ℝ} (hs : 0 < s) :
    P s ↔
      loadRecognitionCost
        (scalePattern s (worldlinePattern gapOneTwoPhaseMode)) = 0 := by
  obtain ⟨hacc, -, huniq⟩ := hsel
  rw [orbit_sigmaZero_iff_eq_factorAmplitude hs]
  constructor
  · intro hPs
    exact huniq s _ hs gapOne_factorAmplitude_pos hPs hacc
  · intro h
    subst h
    exact hacc

/-- The wall in determined form: a selecting genesis predicate is pinned to
the factor-amplitude scale at every positive orbit point. -/
theorem genesisSelection_determined_on_orbit {P : ℝ → Prop}
    (hsel : GenesisSelectsJGround P) {s : ℝ} (hs : 0 < s) :
    P s ↔ s = intendedGapOneFactorAmplitude :=
  (genesisSelection_iff_sigmaZero_on_orbit hsel hs).trans
    (orbit_sigmaZero_iff_eq_factorAmplitude hs)

/-- The two costumes coincide on the orbit: the mass-law genesis predicate
and the σ-zero predicate are the same predicate at every positive scale. -/
theorem massCostume_iff_sigmaZero_on_orbit {s : ℝ} (hs : 0 < s) :
    massLawCostumePredicate s ↔ sigmaZeroOrbitPredicate s := by
  rw [massLawCostume_iff_eq_factorAmplitude hs]
  constructor
  · intro h
    exact ⟨hs, (orbit_sigmaZero_iff_eq_factorAmplitude hs).2 h⟩
  · rintro ⟨-, hcost⟩
    exact (orbit_sigmaZero_iff_eq_factorAmplitude hs).1 hcost

/-- The factor amplitude at the mass law: `f² = predictedMass/16`, the banked
chain `2f² = load·transport = closedAmplitude² = mass/8`. -/
theorem factorAmplitude_sq_eq_predictedMass_div_sixteen :
    intendedGapOneFactorAmplitude ^ 2 =
      predictedMass (worldlinePattern gapOneTwoPhaseMode) / 16 := by
  have hfac := primitivePositiveStationaryFactorAmplitude_sq
    (worldlinePattern gapOneTwoPhaseMode)
  have hclosed := primitiveClosedPatternAmplitude_sq
    (worldlinePattern gapOneTwoPhaseMode)
  have hA := primitiveClosedPatternAmplitude_sq_eq_predictedMass_div_eight
    (worldlinePattern gapOneTwoPhaseMode)
  have hgoal : 2 * intendedGapOneFactorAmplitude ^ 2 =
      predictedMass (worldlinePattern gapOneTwoPhaseMode) / 8 := by
    calc
      2 * intendedGapOneFactorAmplitude ^ 2 =
          primitiveAnchorSectorLoad (worldlinePattern gapOneTwoPhaseMode) *
            primitivePhiTransport (worldlinePattern gapOneTwoPhaseMode) := hfac
      _ = primitiveClosedPatternAmplitude
            (worldlinePattern gapOneTwoPhaseMode) ^ 2 := hclosed.symm
      _ = predictedMass (worldlinePattern gapOneTwoPhaseMode) / 8 := hA
  linarith

What this page does not claim

The value of the factor amplitude f is derived from deeper principles; it is adopted as a MODEL, not proven. The genesis orbit selection wall proves that mass genesis actually occurs; it only classifies rules that select the ground point. The wall applies to orbits other than the gap-one worldline orbit.

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