Masses Mass Genesis T10 Genesis Orbit Selection Wall Factor Amplitude Sq Eq Pred

The mass scale link

The declaration factorAmplitude_sq_eq_predictedMass_div_sixteen is a proved theorem in the framework's machine-checked library of formal theorems. It states that the square of a quantity called the intended gap-one factor amplitude equals the predicted mass of a specific worldline pattern divided by sixteen. In plain terms, it connects a primitive scale factor, a number that describes a fundamental spacing in the framework, to a mass prediction, the quantity the framework associates with a particle. The theorem is a bridge: it shows that the scale factor, which is derived from topology alone, and the mass, which is derived from a separate chain of definitions, are not independent.

To see what this means, consider the framework's account of how a particle's mass arises. The framework models a particle as a pattern on a discrete record of events, called the ledger. A worldline pattern is a specific such pattern, and the framework's machinery assigns it a predicted mass. The factor amplitude is a separate quantity, defined as the unique positive scale at which a certain cost function vanishes along the pattern's scale orbit. The theorem factorAmplitude_sq_eq_predictedMass_div_sixteen asserts that the square of this scale equals the predicted mass divided by sixteen. This is not a numerical coincidence; it is a proved identity within the framework's formal system.

The theorem's role is to support a larger result, the genesis-orbit selection wall. That wall classifies every possible rule for selecting the scale at which a particle is created. The classification shows that any such rule, if it selects the unique vanishing-cost point, is equivalent to the rule that selects the point where the cost is zero. The mass-law costume is one such rule: it selects the scale whose square is the predicted mass over sixteen. The theorem factorAmplitude_sq_eq_predictedMass_div_sixteen is what makes the mass-law costume and the zero-cost rule agree at every positive scale. The framework proves this agreement as a theorem, tagged THEOREM.

What the theorem does not claim is that the predicted mass itself is a measured value. The framework derives the mass from its own definitions, but the comparison against measured particle masses is an empirical check, not a theorem. The theorem also does not claim that the factor amplitude is itself a derived quantity; it is defined by the vanishing-cost condition, and the framework treats that definition as a model choice, not as a forced consequence. Finally, the theorem does not claim that the mass prediction is unique; it only establishes the identity between the scale squared and the mass over sixteen for the specific pattern named in the theorem.

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

/-- 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 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 predicted mass is a measured value. The factor amplitude is itself derived from more primitive principles. The mass prediction is unique across all possible worldline patterns.

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: