Masses Mass Genesis T10 Spring Falsifier Cert Target Constant Law Passes Widened

The widened envelope

The declaration targetConstantLaw_passes_widened_envelope records, in a machine-checked library of formal theorems, that a proposed law for a particle-mass constant satisfies the acceptance test that a frozen, pre-registered protocol had set. The law names a specific amplitude, the factor φ²¹·(√2/4), where φ is the golden ratio. The test has two parts: the law must accept that intended amplitude as the correct one, and it must reject the doubled copy of that amplitude. Both parts pass, and the certificate is measurement-free, meaning no measured value enters the proof.

The subtlety is the envelope, the allowed set of numbers a candidate law may draw on. The frozen protocol had restricted candidates to the rational-φ field, numbers of the form p + qφ with p and q rational. The intended amplitude is not in that field, because it contains √2, and the protocol's own text had named exactly such an outside number as the condition that would reopen the test. The new declaration widens the envelope to the field ℚ(φ)(f), the smallest field containing both the rational-φ numbers and the derived amplitude f. The declaration proves the law passes under this widened envelope, while the original frozen gate text still stands untouched for the narrower class.

What the declaration does not claim is just as important. It does not claim that the amplitude's value is derived from the recognition framework's core cost function; the certificate explicitly separates the derivation from that route. It does not claim the genesis-dynamics reading of the amplitude, a full-dimension coverage principle, which remains open and independent of the deposit normalization. And it does not claim the law passes the original, un-widened gate; the frozen theorem that no law passes that narrower gate remains true. The widened envelope is the falsifier's own authorized escape, and the declaration records that the escape fired.

/-- **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⟩

/-- The amplitude factorization: `f = φ²¹ · (√2 / 4)`, a φ-field rung
scalar times the off-field transport factor. Banked components: C9's
`intended_eq_phi21_mul_creationDepositNorm` and
`creationDepositNorm_eq_sqrt2_div_four`. -/
theorem amplitude_eq_phi21_mul_sqrt2_div_four :
    intendedGapOneFactorAmplitude = Constants.phi ^ 21 * (Real.sqrt 2 / 4) := by
  rw [intended_eq_phi21_mul_creationDepositNorm, creationDepositNorm_eq_sqrt2_div_four]

/-- **√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

/-- **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 declaration does not claim the amplitude's value is derived from the framework's core cost function. The declaration does not claim the genesis-dynamics coverage principle, which remains open. The declaration does not claim the law passes the original, un-widened gate.

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: