Encyclopedia Masses Masses Mass Genesis T10 Scale Law Forcing Wall Orbit Jcost At Amplitude Eq Load

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Scale Law Forcing Wall Orbit Jcost At Amplitude Eq Load

A theorem in the Recognition Science library equates the cost of a rescaled pattern with the cost of the original, tying the search for particle masses to a single mathematical function.

Verify this page

The orbit cost identity

In the Recognition Science framework, a ledger, a discrete record of events, tracks the cost of recognizing a pattern. The theorem orbitJCostAtAmplitude_eq_loadRecognitionCost states that for a settled pattern, the cost of recognizing a rescaled version of that pattern equals the cost of recognizing the original pattern. The cost function is the framework's central object, J(x) = (x + 1/x)/2 - 1, which is forced by five plain conditions. The theorem is a formal identity: it shows that the cost of a pattern at a new scale is the same number as the cost of the original pattern, when the new scale is expressed as a ratio of amplitudes.

The identity is a piece of the T10 scale-law forcing wall, a collection of theorems in the machine-checked library of formal theorems. The wall classifies every principle that could determine a pattern's amplitude, the size of its signal, from a scale-invariant rule. A scale-invariant rule gives the same answer regardless of the overall size of the pattern. The wall proves that such a rule forces the correct amplitude if and only if it admits only one possible value, the primitive factor amplitude. The identity is the bridge that connects the cost function to this classification, showing that the cost extremum, the point of lowest cost, is exactly the singleton set that forces the law.

The theorem does not claim that the cost function itself is derived from the scale law. It does not claim that the amplitude is derived from the cost function alone. It does not claim that any scale-invariant principle works; the wall explicitly shows that a principle admitting both the correct amplitude and three times that amplitude fails to force the law, even though it rejects a doubled decoy. The identity is a formal equivalence, not a physical derivation. It is a theorem about the library's definitions, not a statement about measured particle masses.

What the identity changes is the search for a mass-generation principle. It narrows the field: any viable scale-law principle must be a singleton, and the cost extremum is one such singleton. It does not create the amplitude. It does not explain why the amplitude has the value it does. It shows that the cost function, already forced by the framework's axioms, is the right tool for the job of selecting the amplitude, but it does not say what that amplitude is in physical units.

THEOREM orbitJCostAtAmplitude_eq_loadRecognitionCost · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
orbitJCostAtAmplitude_eq_loadRecognitionCost · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:215 
/-- The orbit J-cost profile agrees with the banked recognition cost of the
rescaled pattern, so the extremization member below IS cost extremization
over the orbit, not a costume. -/
theorem orbitJCostAtAmplitude_eq_loadRecognitionCost
    {a : ℝ} (ha : 0 < a) {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ) (v : ℝ) :
    orbitJCostAtAmplitude ψ v =
      loadRecognitionCost (scalePattern (v / a) ψ) := by
  have hva : v / a * a = v := div_mul_cancel₀ v (ne_of_gt ha)
  have hnorm : normSq8 (neutralize ((scalePattern (v / a) ψ).window 0)) =
      2 * v ^ 2 := by
    have h := settledAnchor_neutralizedNormSq (scalePattern_settledAnchor (v / a) hwin)
    rw [hva] at h
    exact h
  have hpCA : primitiveClosedPatternAmplitude (scalePattern (v / a) ψ) =
      primitiveClosedPatternAmplitude ψ := by
    have hsq : primitiveClosedPatternAmplitude (scalePattern (v / a) ψ) ^ 2 =
        primitiveClosedPatternAmplitude ψ ^ 2 := by
      rw [primitiveClosedPatternAmplitude_sq, primitiveClosedPatternAmplitude_sq,
        ← primitivePositiveStationaryFactorAmplitude_sq,
        ← primitivePositiveStationaryFactorAmplitude_sq,
        primitivePositiveStationaryFactorAmplitude_scalePattern]
    exact (sq_eq_sq₀
      (le_of_lt (primitiveClosedPatternAmplitude_pos _))
      (le_of_lt (primitiveClosedPatternAmplitude_pos _))).1 hsq
  unfold orbitJCostAtAmplitude loadRecognitionCost loadTopologyRatio
  rw [hnorm, hpCA]
THEOREM scaleLawForces_iff_pointwiseSingleton · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
scaleLawForces_iff_pointwiseSingleton · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:122 
/-- **The scale-law forcing dichotomy (THEOREM).** A scale-invariant
scale-law principle forces the load normalization on every settled Q3 orbit
if and only if its admissible class is pointwise trapped inside the σ-zero
singleton. The forward direction transports any positive admissible amplitude
to an actual settled carrier on the same orbit (scaling preserves Q3 evidence
and the settled anchor), reads the law off the forcing hypothesis, and
identifies the transported amplitude with the factor amplitude by the banked
amplitude equation. -/
theorem scaleLawForces_iff_pointwiseSingleton
    {V : ScaleLawPrinciple}
    (hinv : ScaleLawInvariant V) :
    ScaleLawForces V ↔ ScaleLawPointwiseSingleton V := by
  constructor
  · intro hforces ψ E a ha hwin v hv hV
    have hca : 0 < v / a := div_pos hv ha
    have hva : v / a * a = v := div_mul_cancel₀ v (ne_of_gt ha)
    have E' : Q3ClosedPatternEvidence (scalePattern (v / a) ψ) :=
      scalePattern_q3ClosedEvidence (v / a) hca E
    have hwin' : SettledAnchorWindow v (scalePattern (v / a) ψ) := by
      have h := scalePattern_settledAnchor (v / a) hwin
      rw [hva] at h
      exact h
    have hV' : V (scalePattern (v / a) ψ) v := (hinv (v / a) hca ψ v).2 hV
    have hlaw := hforces _ E' hv hwin' hV'
    have heq : v =
        primitivePositiveStationaryFactorAmplitude (scalePattern (v / a) ψ) :=
      (settledAnchor_loadNormalized_iff_amplitude hwin' (le_of_lt hv)).1 hlaw
    rw [primitivePositiveStationaryFactorAmplitude_scalePattern] at heq
    exact heq
  · intro hsingle ψ E a ha hwin hVa
    have heq := hsingle ψ E ha hwin ha hVa
    exact (settledAnchor_loadNormalized_iff_amplitude hwin (le_of_lt ha)).2 heq
THEOREM tripleFactorAdmissible_not_forcing · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
tripleFactorAdmissible_not_forcing · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:362 
/-- **Non-singleton members do not force (THEOREM, exhibited).** A settled Q3
carrier at triple the factor amplitude satisfies the triple-factor assertion
and fails the load-normalization law. -/
theorem tripleFactorAdmissible_not_forcing :
    ∃ (ψ : LightPattern (Fin 8)) (a : ℝ),
      0 < a ∧ Q3MatterCarrier ψ ∧ SettledAnchorWindow a ψ ∧
        tripleFactorAdmissible ψ a ∧ ¬ LoadNormalizedToTopology ψ := by
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  obtain ⟨c, hc, hload⟩ := exists_scale_loadNormalizedToTopology Eseed
  have hseed : SettledAnchorWindow 1 (worldlinePattern gapOneTwoPhaseMode) := by
    unfold SettledAnchorWindow
    funext t
    simp [worldlinePattern, commitSettlementWindow_zero_eq_gapOne]
  have hground : SettledAnchorWindow c
      (scalePattern c (worldlinePattern gapOneTwoPhaseMode)) := by
    simpa using scalePattern_settledAnchor c hseed
  have Eground : Q3ClosedPatternEvidence
      (scalePattern c (worldlinePattern gapOneTwoPhaseMode)) :=
    scalePattern_q3ClosedEvidence c hc Eseed
  have hcf : c = primitivePositiveStationaryFactorAmplitude
      (scalePattern c (worldlinePattern gapOneTwoPhaseMode)) :=
    (settledAnchor_loadNormalized_iff_amplitude hground (le_of_lt hc)).1 hload
  let χ := scalePattern 3 (scalePattern c (worldlinePattern gapOneTwoPhaseMode))
  have Eχ : Q3ClosedPatternEvidence χ :=
    scalePattern_q3ClosedEvidence 3 (by norm_num) Eground
  have hχwin : SettledAnchorWindow (3 * c) χ := by
    simpa [χ] using scalePattern_settledAnchor 3 hground
  have hfχ : primitivePositiveStationaryFactorAmplitude χ =
      primitivePositiveStationaryFactorAmplitude
        (scalePattern c (worldlinePattern gapOneTwoPhaseMode)) :=
    primitivePositiveStationaryFactorAmplitude_scalePattern _ _
  have h3c : 0 < 3 * c := mul_pos (by norm_num) hc
  refine ⟨χ, 3 * c, h3c, ⟨Eχ⟩, hχwin, ?_, ?_⟩
  · right
    rw [hfχ, ← hcf]
  · intro hlaw
    have heq := (settledAnchor_loadNormalized_iff_amplitude hχwin
      (le_of_lt h3c)).1 hlaw
    rw [hfχ, ← hcf] at heq
    nlinarith [hc]

What this page does not claim

The theorem does not derive the value of the primitive factor amplitude from the cost function. The theorem does not state that the cost function is the only possible scale-law principle. The theorem does not claim that the amplitude is a measured physical quantity.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND