Masses Mass Genesis T10 Genesis Orbit Selection Wall Genesis Selection Iff Sigma

The selection wall

The declaration genesisSelection_iff_sigmaZero_on_orbit is a theorem in the machine-checked library of formal theorems that Recognition Science builds on. It answers a narrow question: suppose some rule, any rule, selects the one special point on a particle's scale orbit, the point where the framework's cost (a number measuring how expensive a recognition event is) vanishes. The theorem says that any such rule is, point by point on that orbit, exactly the rule “the cost is zero.” No matter what constants or form the rule uses, its selection content collapses to that single equation.

To see why this matters, picture a particle's possible scales as a line of positive numbers. The framework's cost function J(x) = (x + 1/x)/2 - 1 has a unique minimum at x = 1, where it is zero. For a specific worldline pattern, scaling by a factor s produces a cost that vanishes at exactly one positive scale, called the factor amplitude f. The theorem's normal form, orbit_sigmaZero_iff_eq_factorAmplitude, states this: along the orbit, cost equals zero if and only if s equals f. The selection wall then says any predicate that accepts f, rejects its double 2f, and pins down at most one positive scale, is forced to be the cost-zero predicate on that orbit.

The framework exhibits two natural costumes for this same predicate. One, sigmaZeroOrbitPredicate, is the direct statement “the cost is zero.” The other, massLawCostumePredicate, is dressed as “the square of the scale equals the predicted mass divided by sixteen.” A separate theorem, massCostume_iff_sigmaZero_on_orbit, proves these two faces agree at every positive orbit point. The factor amplitude f itself satisfies f² = mass/16, which is why the mass-law costume works. The wall certifies that both costumes select the same point, and that no other rule can select it differently.

What the theorem does not claim is just as important. It does not say that such a selecting rule exists; it classifies rules that already satisfy the gate. It does not say the cost-zero content is derived from first principles; that content is adopted as a foundational model, not proved. It does not say anything about scales outside the gap-one worldline orbit. And it does not say the factor amplitude f is rational or constructible from simple constants; in fact, a companion result shows f is not in the rational-φ field, which is why the selector side cannot supply it from banked emission absolutes.

The consequence is a clean classification: on the genesis side, the escape from the inhomogeneity wall is a theorem-tier derivation of the cost-zero selection content itself. Until that derivation exists, the unique selector remains a model law, not a proved one. The wall makes the missing map exact on both sides, and names the one object both sides point to.

/-- **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 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 theorem does not prove that any selecting rule exists; it classifies rules that already satisfy the gate. The theorem does not derive the sigma-zero content from first principles; that content is adopted as a model. The theorem does not apply to scales outside 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: