Encyclopedia Masses Masses Mass Genesis T10 Spring Falsifier Cert

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Spring Falsifier Cert

A pre-registered test for whether a new particle-mass constant was derived or just assumed has fired, and the machine-checked certificate records the result.

Verify this page

The spring audit

The ledger, a discrete record of recognition events, tracks every value the framework uses. A frozen gate, a set of fixed rules, once blocked a candidate constant because it sat outside the allowed field of numbers. The spring audit is the formal record of that gate reopening after a new derivation supplied the missing piece.

The candidate is the emission amplitude f = φ²¹ · (1/√2)³, a number built from the golden ratio φ and a square root of two. The frozen gate required all derived constants to live in the rational-φ field, numbers of the form p + qφ with p and q rational. The square root of two is not in that field, so f was blocked. The pre-registered falsifier, a reopening condition written into the gate, said the block could be lifted if a premise-free derivation produced an emission-side absolute outside that field. That derivation arrived, dated after the freeze, and the certificate records the firing.

The module proves the constant now passes the gate under a widened envelope, the field ℚ(φ)(f). It shows the envelope is closed under addition, multiplication, and inverses, and that every element has a unique representation. It also proves the square root of two is genuinely outside the original field, so the escape is real, not a relabeling. The gate's other clauses, acceptance of the intended witness and rejection of its doubled copy, pass unchanged.

In Recognition Science, this matters because it separates a derived value from an assumed one. Before the new derivation, naming f required the very inhomogeneity the gate existed to reject. After it, the agreement between the derived constant and the σ-zero amplitude is a theorem about two independent routes landing on one value. The certificate explicitly does not claim the inhomogeneity itself; it claims the envelope widened, and the frozen gate text stands untouched.

THEOREM targetConstantLaw_passes_widened_envelope · IndisputableMonolith/Masses/MassGenesis/T10SpringFalsifierCert.lean
targetConstantLaw_passes_widened_envelope · IndisputableMonolith/Masses/MassGenesis/T10SpringFalsifierCert.lean:437 
/-- **The selector promotes.** Under the widened envelope the wall's
unique discriminating member passes all three clauses: clause (i) by the
fired falsifier (`u = 1` from the frozen census, `C = f` newly derived),
clauses (ii) and (iii) banked unchanged. -/
theorem targetConstantLaw_passes_widened_envelope :
    PassesSelectorGateWidenedEnvelope targetConstantLaw :=
  ⟨inDerivedEnvelope_one, inDerivedEnvelope_amplitude,
   targetConstantLaw_accepts_intended, targetConstantLaw_rejects_doubled⟩
THEOREM sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10SpringFalsifierCert.lean
sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10SpringFalsifierCert.lean:192 
/-- **√2 ∉ ℚ(φ).** The off-field factor's base is not a rational-φ
combination. The representation `√2 = p + qφ` would force
`2pq + q² = 0` and `p² + q² = 2` (rational independence of `{1, φ}`); the
first case gives `p² = 2` and the second `(5p)² = 10`, and both `2` and
`10` are `≡ 2 mod 4`, which no perfect square is. Since
`φ = (1 + √5)/2` we have `ℚ(φ) = ℚ(√5)`, so this is exactly
"√2 ∉ ℚ(√5)". -/
theorem sqrt_two_not_inQPhi : ¬ InQPhi (Real.sqrt 2) := by
  rintro ⟨p, q, h⟩
  have h1 : (Real.sqrt 2) ^ 2 = (2 : ℝ) := Real.sq_sqrt (by norm_num)
  have h2 : ((p : ℝ) + (q : ℝ) * Constants.phi) ^ 2 = (2 : ℝ) := by
    rw [← h]; exact h1
  have heq : (((p ^ 2 + q ^ 2 : ℚ) : ℝ)) + (((2 * p * q + q ^ 2 : ℚ) : ℝ)) *
        Constants.phi =
      (((2 : ℚ) : ℝ)) + (((0 : ℚ) : ℝ)) * Constants.phi := by
    push_cast
    linear_combination h2 - ((q : ℝ) ^ 2) * Constants.phi_sq_eq
  obtain ⟨hA, hB⟩ := rat_coeff_eq_of_phi_spring heq
  have hfactor : q * (2 * p + q) = (0 : ℚ) := by linear_combination hB
  rcases mul_eq_zero.mp hfactor with hq0 | h2pq
  · subst hq0
    have hp2 : (p : ℝ) ^ 2 = (2 : ℝ) := by
      have hp2q : p ^ 2 = (2 : ℚ) := by linear_combination hA
      exact_mod_cast hp2q
    exact not_rat_sq_of_mod_four_spring 2 (by norm_num) p hp2
  · have hqeq : q = -2 * p := by linear_combination h2pq
    have hq2 : q ^ 2 = 4 * p ^ 2 := by rw [hqeq]; ring
    have h10 : (5 * p) ^ 2 = (10 : ℚ) := by linear_combination 5 * hA - 5 * hq2
    have h10R : ((5 * p : ℚ) : ℝ) ^ 2 = (10 : ℝ) := by exact_mod_cast h10
    exact not_rat_sq_of_mod_four_spring 10 (by norm_num) (5 * p) h10R
THEOREM targetConstantLaw_passes_widened_envelope · IndisputableMonolith/Masses/MassGenesis/T10SpringFalsifierCert.lean
targetConstantLaw_passes_widened_envelope · IndisputableMonolith/Masses/MassGenesis/T10SpringFalsifierCert.lean:437 
/-- **The selector promotes.** Under the widened envelope the wall's
unique discriminating member passes all three clauses: clause (i) by the
fired falsifier (`u = 1` from the frozen census, `C = f` newly derived),
clauses (ii) and (iii) banked unchanged. -/
theorem targetConstantLaw_passes_widened_envelope :
    PassesSelectorGateWidenedEnvelope targetConstantLaw :=
  ⟨inDerivedEnvelope_one, inDerivedEnvelope_amplitude,
   targetConstantLaw_accepts_intended, targetConstantLaw_rejects_doubled⟩
THEOREM frozen_gate_text_stands · IndisputableMonolith/Masses/MassGenesis/T10SpringFalsifierCert.lean
frozen_gate_text_stands · IndisputableMonolith/Masses/MassGenesis/T10SpringFalsifierCert.lean:446 
/-- **The frozen text stands.** Nothing here edits or weakens the frozen
wall: over the frozen class with the frozen envelope, no law passes, now
and permanently. The widening is a new derivation, not a renegotiation:
the falsifier's conjuncts are met by kernel theorems that did not exist at
freeze time. -/
theorem frozen_gate_text_stands :
    ∀ L : FieldCurrentMagnitudeLaw, ¬ PassesSelectorGate L :=
  no_fieldCurrentLaw_passes_selectorGate

What this page does not claim

The inhomogeneity R4 is derived or assumed. The value f is measured or compared against experiment. The genesis-dynamics reading of the off-field factor is closed. The frozen gate's original verdict is overturned.

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/T10SpringFalsifierCert.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