Encyclopedia Masses Masses Mass Genesis T10 Scale Law Forcing Wall J Extremum Admissible Iff Eq Fact

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Scale Law Forcing Wall J Extremum Admissible Iff Eq Fact

A proposed rule for fixing particle masses by minimizing a cost function succeeds only when it selects a single, specific amplitude, and that amplitude is the framework's ground state.

Verify this page

The cost minimum is the mass

The declaration recognition (a discrete record of events) science asks how the masses of particles get their values. One candidate answer is an extremum principle: the physical amplitude is the one that minimizes some cost. The theorem jExtremumAdmissible_iff_eq_factorAmplitude states that this principle is equivalent to a much simpler condition. For any settled pattern, the set of admissible amplitudes is exactly the singleton set containing the primitive factor amplitude. In plain words, the cost-minimizing amplitude exists, is unique, and equals the framework's ground-state amplitude.

The theorem is not a derivation of the mass law from scratch. It shows that the cost-extremization principle is a member of a larger class of scale-invariant principles, and that within that class it is the one that forces the law. The framework's library proves that any such forcing principle is pointwise equivalent to the statement that the recognition cost is zero. So the extremum principle is not an independent source of the mass law; it is the ground-state selection in disguise.

The theorem also rules out a tempting alternative. A principle that admits both the factor amplitude and three times that amplitude is scale-invariant and rejects the doubled decoy, yet it fails to force the law. A settled carrier at the triple amplitude satisfies the principle but violates the law. This shows that rejecting the doubled decoy is not enough; the admissible set must be a singleton.

What the theorem does not claim is that the extremum principle is the only way to force the law. It classifies the class of scale-invariant principles, and a genuinely inhomogeneous functional would escape the classification. The library's homogeneity record says none exists at theorem tier, but supplying one is an open campaign, not a route inside the library.

THEOREM jExtremumAdmissible_iff_eq_factorAmplitude · 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
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 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 prove that the extremum principle is the only possible forcing principle. It does not derive the mass law from a non-topological principle; it shows the extremum principle is equivalent to the ground-state condition. It does not claim that a principle admitting the triple amplitude is adequate; that principle fails to force the law.

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