Encyclopedia Masses Masses Mass Genesis T10 Scale Law Forcing Wall Scale Law Admissible Iff Eq Facto

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Scale Law Forcing Wall Scale Law Admissible Iff Eq Facto

A theorem in the Recognition Science framework shows that any scale-invariant rule for particle masses either picks exactly one value or fails to force the mass law.

Verify this page

The scale-law wall

In the Recognition Science framework, the mass of a particle is not a free parameter but a consequence of how a pattern of eight recognition events settles. The framework's library, a machine-checked collection of formal theorems, models this with a quantity called the primitive factor amplitude, the single amplitude the settled pattern must carry. A scale-law principle is any proposed rule that tries to derive this amplitude from something else, such as minimizing a cost or conserving a ledger, a discrete record of events. The theorem scale-law wall classifies every such rule at once.

The theorem scaleLaw_admissible_iff_eq_factorAmplitude_of_forces states the classification. For any scale-invariant and adequate scale-law principle that forces the mass law, the rule's admissible amplitudes are exactly the primitive factor amplitude. In plainer terms: if a rule is to work, it cannot allow two different mass values; it must single out the one the settled pattern already carries. The proof shows that any such principle is equivalent to the statement that the recognition cost is zero, the ground-state selection, and that the cost-extremization principle is the canonical member of the class. A decoy that rejects the doubled amplitude but allows the triple one fails to force the law, so rejecting one wrong value does not rescue a rule.

The wall's scope is precise. It covers every principle whose admissible set is scale-invariant, meaning the rule does not depend on the absolute size of the pattern. The library records that no inhomogeneous functional exists at theorem tier, so no rule escapes the wall that way. The theorem does not claim that the primitive factor amplitude is derived from first principles; it claims that any successful scale-law principle must land on that amplitude, not that the amplitude itself is explained. The theorem also does not claim that a creation operator exists; that remains an open target. What the wall establishes is a negative result with a positive core: the mass law is not derivable from a wider class of principles, and the only viable route is the one the framework already banks.

THEOREM scaleLaw_admissible_iff_eq_factorAmplitude_of_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
scaleLaw_admissible_iff_eq_factorAmplitude_of_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:155 
/-- Under adequacy, a forcing principle's admissible class is exactly the
σ-zero singleton on every settled Q3 orbit. -/
theorem scaleLaw_admissible_iff_eq_factorAmplitude_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 : ℝ} (hv : 0 < v) :
    V ψ v ↔ v = primitivePositiveStationaryFactorAmplitude ψ := by
  have hsingle := (scaleLawForces_iff_pointwiseSingleton hinv).1 hforces
  constructor
  · exact hsingle ψ E ha hwin hv
  · intro h
    rw [h]
    exact had ψ E ha hwin
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]
THEOREM scaleLaw_admissible_iff_eq_factorAmplitude_of_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean
scaleLaw_admissible_iff_eq_factorAmplitude_of_forces · IndisputableMonolith/Masses/MassGenesis/T10ScaleLawForcingWall.lean:155 
/-- Under adequacy, a forcing principle's admissible class is exactly the
σ-zero singleton on every settled Q3 orbit. -/
theorem scaleLaw_admissible_iff_eq_factorAmplitude_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 : ℝ} (hv : 0 < v) :
    V ψ v ↔ v = primitivePositiveStationaryFactorAmplitude ψ := by
  have hsingle := (scaleLawForces_iff_pointwiseSingleton hinv).1 hforces
  constructor
  · exact hsingle ψ E ha hwin hv
  · intro h
    rw [h]
    exact had ψ E ha hwin

What this page does not claim

The primitive factor amplitude is not derived from first principles; the theorem only says successful rules must land on it. No creation-like operator is supplied or assumed; deriving one remains an open campaign. The wall does not cover a genuinely inhomogeneous functional, which would escape the classification.

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