Encyclopedia Masses Masses Mass Genesis T10 Scale Law Forcing Wall

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Scale Law Forcing Wall

A machine-checked proof that no scale-invariant principle can independently derive the particle mass law; it can only restate the framework's ground-state condition.

Verify this page

The scale-law wall

A scale law in physics is a rule that fixes a quantity's size. The framework under test here, Recognition Science, asks whether its own law for particle masses, called load normalization (the rule that a pattern's normalized amplitude equals its primitive anchor amplitude squared), can be forced from a more basic principle. The question matters because a derived law would be independent; a restated one would not.

The module examines a whole class of candidate principles. Each one asserts that the physical anchor amplitude lies in some computed admissible set. The class is defined by a single property: the admissible set is scale-invariant, meaning it does not change when the pattern is rescaled. The framework's library, a machine-checked collection of formal theorems, proves a classification result for this entire class at once.

The main theorem, scaleLawForces_iff_pointwiseSingleton, states that a scale-invariant principle forces the load normalization law on every settled orbit if and only if its admissible set is a singleton: the only positive admissible amplitude is the primitive factor amplitude itself. A second theorem, scaleLaw_assertion_iff_sigmaZero_of_forces, shows that under adequacy, any such forcing principle's assertion is pointwise equivalent to the statement that the recognition cost is zero. The principle is therefore the R4 ground-state selection in assertion costume, never an independent derivation of the law.

The canonical member of this class is the J-cost extremum, the principle that the admissible amplitude minimizes the orbit's J-cost profile. The theorem jExtremumAdmissible_iff_eq_factorAmplitude proves this principle is adequate, forces, and selects exactly the primitive factor amplitude. Cost extremization exists, selects the right point, and is R4.

The wall is sharp. The principle that admits both the primitive factor amplitude and three times it, tripleFactorAdmissible, is scale-invariant and adequate, and it rejects the doubled decoy. Yet the theorem tripleFactorAdmissible_not_forcing shows it fails to force the law on a settled carrier at amplitude three times the factor. Rejecting the doubled decoy does not rescue a non-singleton member.

The scope is precise. A genuinely inhomogeneous functional would escape the class, but the library's homogeneity record says none exists at theorem tier. Supplying one is a separate campaign, not a route inside the library. The wall classifies what the library can state; it does not close the question of what a future, richer library might say.

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_iff_eq_factorAmplitude · jExtremumAdmissible_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
jExtremumAdmissible_iff_eq_factorAmplitude · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:250 
/-- **Cost extremization is the σ-zero singleton (THEOREM).** The orbit
J-cost is minimized at exactly the primitive factor amplitude: J vanishes
only at ratio one, the profile attains zero at `v = f`, and every minimizer
must therefore have `(v / f)² = 1`. -/
theorem jExtremumAdmissible_iff_eq_factorAmplitude
    (ψ : LightPattern (Fin 8)) {v : ℝ} :
    jExtremumAdmissible ψ v ↔
      v = primitivePositiveStationaryFactorAmplitude ψ := by
  have hp : 0 < primitivePositiveStationaryFactorAmplitude ψ :=
    factorAmplitude_pos ψ
  have hpCA2 : 0 < primitiveClosedPatternAmplitude ψ ^ 2 :=
    pow_pos (primitiveClosedPatternAmplitude_pos ψ) 2
  have h2f : 2 * primitivePositiveStationaryFactorAmplitude ψ ^ 2 =
      primitiveClosedPatternAmplitude ψ ^ 2 := by
    rw [primitivePositiveStationaryFactorAmplitude_sq ψ,
      primitiveClosedPatternAmplitude_sq ψ]
  have hratio_f : 2 * primitivePositiveStationaryFactorAmplitude ψ ^ 2 /
      primitiveClosedPatternAmplitude ψ ^ 2 = 1 := by
    rw [h2f]
    exact div_self (ne_of_gt hpCA2)
  constructor
  · intro h
    obtain ⟨hv, hmin⟩ := h
    have harg : 0 < 2 * v ^ 2 / primitiveClosedPatternAmplitude ψ ^ 2 :=
      div_pos (mul_pos (by norm_num) (pow_pos hv 2)) hpCA2
    have hle := hmin _ hp
    unfold orbitJCostAtAmplitude at hle
    rw [hratio_f, IndisputableMonolith.Cost.Jcost_unit0] at hle
    have hge : 0 ≤ orbitJCostAtAmplitude ψ v :=
      IndisputableMonolith.Cost.Jcost_nonneg harg
    have hJ0 : orbitJCostAtAmplitude ψ v = 0 := le_antisymm hle hge
    have hJ0' : IndisputableMonolith.Cost.Jcost
        (2 * v ^ 2 / primitiveClosedPatternAmplitude ψ ^ 2) = 0 := hJ0
    have hratio1 : 2 * v ^ 2 / primitiveClosedPatternAmplitude ψ ^ 2 = 1 :=
      (IndisputableMonolith.Cost.Jcost_eq_zero_iff _ harg).1 hJ0'
    have hvsq : 2 * v ^ 2 = primitiveClosedPatternAmplitude ψ ^ 2 := by
      have hne : primitiveClosedPatternAmplitude ψ ^ 2 ≠ 0 := ne_of_gt hpCA2
      have hmc := div_mul_cancel₀ (2 * v ^ 2) hne
      rw [hratio1] at hmc
      linarith
    have hv2 : v ^ 2 = primitivePositiveStationaryFactorAmplitude ψ ^ 2 := by
      linarith
    exact (sq_eq_sq₀ (le_of_lt hv) (le_of_lt hp)).1 hv2
  · intro h
    subst h
    refine ⟨hp, fun w hw => ?_⟩
    have harg : 0 < 2 * w ^ 2 / primitiveClosedPatternAmplitude ψ ^ 2 :=
      div_pos (mul_pos (by norm_num) (pow_pos hw 2)) hpCA2
    unfold orbitJCostAtAmplitude
    rw [hratio_f, IndisputableMonolith.Cost.Jcost_unit0]
    exact IndisputableMonolith.Cost.Jcost_nonneg harg
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_scaleInvariant · tripleFactorAdmissible_adequate · tripleFactorAdmissible_rejects_doubled · tripleFactorAdmissible_not_forcing · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
tripleFactorAdmissible_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:337 
theorem tripleFactorAdmissible_scaleInvariant :
    ScaleLawInvariant tripleFactorAdmissible := by
  intro c hc ψ v
  show (v = primitivePositiveStationaryFactorAmplitude (scalePattern c ψ) ∨
        v = 3 * primitivePositiveStationaryFactorAmplitude (scalePattern c ψ)) ↔
      (v = primitivePositiveStationaryFactorAmplitude ψ ∨
        v = 3 * primitivePositiveStationaryFactorAmplitude ψ)
  rw [primitivePositiveStationaryFactorAmplitude_scalePattern]
tripleFactorAdmissible_adequate · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:346 
theorem tripleFactorAdmissible_adequate :
    ScaleLawAdequate tripleFactorAdmissible := by
  intro ψ E a ha hwin
  exact Or.inl rfl
tripleFactorAdmissible_rejects_doubled · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:351 
/-- The triple-factor principle rejects the doubled decoy on every
pattern. -/
theorem tripleFactorAdmissible_rejects_doubled
    (ψ : LightPattern (Fin 8)) :
    ¬ tripleFactorAdmissible ψ
      (2 * primitivePositiveStationaryFactorAmplitude ψ) := by
  have hp := factorAmplitude_pos ψ
  intro hmem
  unfold tripleFactorAdmissible at hmem
  rcases hmem with h | h <;> nlinarith [hp]
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 wall does not prove that no scale law can be derived from a non-topological principle; it classifies only the scale-invariant class. The wall does not supply a creation operator or any route to deriving one. The wall does not claim that the load normalization law itself is false or unforced; it shows it is equivalent to R4.

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