Masses Mass Genesis T10 Genesis Orbit Selection Wall Sigma Zero Orbit Predicate

A single allowed scale

In the Recognition Science framework, a ledger is a discrete record of recognition events, and recognition is the act of registering one. The declaration sigmaZeroOrbitPredicate_rejects_doubled is a theorem about a specific rule for choosing a scale at which a particle's mass is created. The rule, called the sigma-zero orbit predicate, says: accept a positive scale if and only if the recognition cost of the worldline pattern at that scale is exactly zero. The theorem states that this rule rejects the doubled scale, meaning it does not accept the scale that is twice the intended factor amplitude.

The proof is short and relies on a stronger result: along the scale orbit of the gap-one worldline seed, the recognition cost vanishes at exactly one positive scale, the primitive factor amplitude. The doubled scale is a different positive scale, so it cannot be the one where the cost vanishes. This is a formal, machine-checked derivation in the framework's library of formal theorems. It is part of a larger wall of results showing that any genesis-creation predicate that selects the J-ground point is, pointwise on the positive orbit, the sigma-zero predicate itself.

What this theorem does not claim is broader. It does not claim that the sigma-zero predicate is the only possible genesis rule; it only shows that any rule which selects the J-ground point must agree with it on the orbit. It does not claim that the sigma-zero predicate is derived from first principles; it is a definitional choice, a MODEL in the framework's terminology. The theorem does not establish that the factor amplitude is the actual measured mass of any particle; that comparison is an empirical check, not a theorem. The theorem is a precise statement about the logical consequences of a definition, not a physical discovery.

theorem sigmaZeroOrbitPredicate_rejects_doubled :
    ¬ sigmaZeroOrbitPredicate (2 * intendedGapOneFactorAmplitude) := by
  rintro ⟨hpos, hcost⟩
  have h := (orbit_sigmaZero_iff_eq_factorAmplitude hpos).1 hcost
  have hf := gapOne_factorAmplitude_pos
  linarith

/-- **Orbit normal form (THEOREM).** Along the scale orbit of the gap-one
worldline seed, the load-recognition `J`-cost vanishes at exactly one
positive scale: the primitive factor amplitude. Assembled from the banked
kernel iff on settled anchors and the topology-only scale invariance of the
factor amplitude. -/
theorem orbit_sigmaZero_iff_eq_factorAmplitude {s : ℝ} (hs : 0 < s) :
    loadRecognitionCost
        (scalePattern s (worldlinePattern gapOneTwoPhaseMode)) = 0 ↔
      s = intendedGapOneFactorAmplitude := by
  obtain ⟨E⟩ := q3MatterCarrier_worldlinePattern_gapOne
  have hunit : SettledAnchorWindow 1 (worldlinePattern gapOneTwoPhaseMode) := by
    unfold SettledAnchorWindow
    funext t
    simp [worldlinePattern, commitSettlementWindow_zero_eq_gapOne]
  have Escaled := scalePattern_q3ClosedEvidence s hs E
  have hscaled :
      SettledAnchorWindow s
        (scalePattern s (worldlinePattern gapOneTwoPhaseMode)) := by
    simpa using scalePattern_settledAnchor s hunit
  have hiff := settledAnchor_loadRecognitionCost_zero_iff_amplitude
    Escaled hscaled (le_of_lt hs)
  rw [primitivePositiveStationaryFactorAmplitude_scalePattern] at hiff
  exact hiff

/-- **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

What this page does not claim

The sigma-zero predicate is the only possible genesis rule. The factor amplitude is a derived physical constant. The theorem establishes the measured mass of any particle.

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: