Encyclopedia Masses Masses Mass Genesis T10 Scale Law Forcing Wall Scale Law Assertion Iff Sigma Zer

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Scale Law Forcing Wall Scale Law Assertion Iff Sigma Zer

A machine-checked theorem classifies every candidate law for particle masses, showing they all reduce to one ground-state condition.

Verify this page

The wall's verdict

A scale law is a rule that tries to pick out the correct amplitude, or strength, of a particle's pattern from a list of possible values. The framework's library of formal theorems proves a sweeping result about such rules: if a rule is scale-invariant, meaning it makes the same choice regardless of the overall size of the pattern, and if it actually succeeds in forcing the correct load-normalized topology on every settled orbit, then its assertion is equivalent to a single condition. That condition is that the recognition cost equals zero. The theorem scaleLaw_assertion_iff_sigmaZero_of_forces states this equivalence precisely: under the assumptions of scale invariance, adequacy, and forcing, the rule's assertion holds exactly when loadRecognitionCost ψ = 0.

This is a classification result, not a new derivation. It says that any scale-invariant principle that works is, in effect, the R4 ground-state selection wearing a different costume. It does not provide a new way to derive the load-normalization law; it shows that all viable candidates in this class are equivalent to the same underlying condition. The theorem also identifies a specific member of this class: the J-cost extremum, which selects the amplitude that minimizes the orbit cost, is itself a forcing principle and is pointwise equivalent to the zero-cost singleton. This means cost extremization is not a separate route; it is the same selection criterion expressed in a different form.

The theorem also exposes a boundary. A principle that allows both the true factor amplitude and three times that amplitude is scale-invariant and adequate, and it rejects the doubled decoy, yet it fails to force the law. A settled carrier at three times the factor amplitude satisfies the principle's assertion while violating the load-normalized topology. This counterexample shows that rejecting one bad candidate is not enough; the admissible set must be a singleton for the principle to force the law.

In Recognition Science, this wall closes a specific door. It proves that no scale-invariant principle can independently derive the load-normalization law; any such principle that works is the zero-cost condition in disguise. The result does not touch a different door, one involving a creation operator with continuum-many deposit points, which remains open. The theorem is a wall against a class of derivations, not a claim that no derivation exists.

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 scaleLaw_assertion_iff_sigmaZero_of_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
scaleLaw_assertion_iff_sigmaZero_of_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:193 
/-- The σ-zero form: a forcing principle's assertion is exactly the vanishing
of the load-recognition J-cost, the R4 ground-state selection restated as an
admissibility assertion. No forcing member of the class is an independent
derivation of the law. -/
theorem scaleLaw_assertion_iff_sigmaZero_of_forces
    {V : ScaleLawPrinciple}
    (hinv : ScaleLawInvariant V)
    (had : ScaleLawAdequate V)
    (hforces : ScaleLawForces V)
    {ψ : LightPattern (Fin 8)} (E : Q3ClosedPatternEvidence ψ)
    {a : ℝ} (ha : 0 < a) (hwin : SettledAnchorWindow a ψ) :
    V ψ a ↔ loadRecognitionCost ψ = 0 :=
  (scaleLaw_assertion_iff_law_of_forces hinv had hforces E ha hwin).trans
    (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).symm
THEOREM jExtremumAdmissible_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
jExtremumAdmissible_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:318 
/-- The J-cost extremization principle forces the law, and is therefore
(pointwise) R4 itself: the only cost-extremization derivation of the load
normalization is the ground-state selection restated. -/
theorem jExtremumAdmissible_forces :
    ScaleLawForces jExtremumAdmissible := by
  intro ψ E a ha hwin hVa
  exact (settledAnchor_loadNormalized_iff_amplitude hwin (le_of_lt ha)).2
    ((jExtremumAdmissible_iff_eq_factorAmplitude ψ).1 hVa)
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 load-normalization law from a non-topological principle. The theorem does not claim that no derivation of the law exists, only that no scale-invariant principle can provide one. The theorem does not address Door B, the creation operator with continuum-many deposit points, which remains untouched.

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