Masses Mass Genesis T10 Spring Falsifier Cert Derived Envelope Repr Unique

The unique envelope representation

In mathematics, a representation theorem tells you when two different-looking expressions actually describe the same object. The declaration derivedEnvelope_repr_unique is such a theorem. It concerns numbers of the form u + v·f, where u and v are drawn from a specific field of numbers built from the golden ratio, and f is a newly derived amplitude value. The theorem states that if two such expressions are equal, then their corresponding coefficients u and v must be identical. In plainer terms, there is exactly one way to write any number in this extended system as a combination of a golden-ratio-field part and an amplitude part.

This uniqueness is not automatic. The golden-ratio field, denoted ℚ(φ), consists of numbers of the form p + q·φ with p and q rational. It is closed under addition, multiplication, and division, but it does not contain the square root of 2. The newly derived amplitude f equals φ²¹·(√2/4), which lies outside this field precisely because of that square root. By adjoining f to the golden-ratio field, one obtains a larger field, and the representation theorem guarantees that this extension behaves cleanly: each element has a unique coordinate pair. This is a standard and desirable property in field theory, akin to how complex numbers have a unique representation as a + b·i.

The theorem is proved in the framework's machine-checked library of formal theorems, with no unproved axioms and no measurement inputs. It is a purely structural result about the number system, not a physical claim. It does not assert that the amplitude f is the correct value for any physical process, nor does it derive f from first principles. The derivation of f itself is a separate matter, documented elsewhere. What this theorem does is ensure that once f is introduced, the mathematical language used to describe it is unambiguous, a necessary foundation for any further work that builds on this value.

In the context of the spring audit, this uniqueness result supports a wider claim: that a previously frozen selection criterion, which had rejected the amplitude as outside its permitted envelope, can be legitimately widened to include it. The uniqueness theorem is one of several ingredients in that adjudication. It is not, however, the reason the amplitude was derived; it is a consistency check on the mathematical framework after the fact. The practical consequence is that the framework can now speak about this amplitude with the same precision it uses for golden-ratio numbers, without ambiguity or hidden assumptions about how to decompose expressions.

/-- The representation in the widened envelope is unique: the extension is
genuinely quadratic, with `f ∉ ℚ(φ)` doing the work. -/
theorem derivedEnvelope_repr_unique {u v u' v' : ℝ}
    (hu : InQPhi u) (hv : InQPhi v) (hu' : InQPhi u') (hv' : InQPhi v')
    (h : u + v * intendedGapOneFactorAmplitude =
      u' + v' * intendedGapOneFactorAmplitude) :
    u = u' ∧ v = v' := by
  by_cases hvv : v = v'
  · subst hvv
    refine ⟨?_, rfl⟩
    linarith
  · exfalso
    have hv0 : v - v' ≠ 0 := sub_ne_zero.mpr hvv
    have h1 : (v - v') * intendedGapOneFactorAmplitude = u' - u := by
      linarith
    have hf : intendedGapOneFactorAmplitude = (u' - u) / (v - v') := by
      rw [← mul_div_cancel_right₀ intendedGapOneFactorAmplitude hv0]
      rw [show intendedGapOneFactorAmplitude * (v - v') =
        (v - v') * intendedGapOneFactorAmplitude by ring, h1]
    exact intendedGapOneFactorAmplitude_not_inQPhi
      (hf ▸ (hu'.add hu.neg).div (hv.add hv'.neg) hv0)

/-- 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]

theorem springFalsifierFiredCert : SpringFalsifierFiredCert where
  emission_side :=
    ⟨gapOne_factorAmplitude_pos,
     by simpa [intendedGapOneFactorAmplitude] using
       gapOne_factorAmplitude_sq_eq_phi42_div_eight,
     intended_eq_phi21_mul_creationDepositNorm⟩
  outside_qphi := intendedGapOneFactorAmplitude_not_inQPhi
  sqrt2_outside_qphi := sqrt_two_not_inQPhi
  amplitude_factorization := amplitude_eq_phi21_mul_sqrt2_div_four
  yardstick_certified := r0_ew_certified_eq_55
  exponent_derived := derivedMassExponent_eq_42
  rung_scalar_in_qphi := inQPhi_phi_pow 21
  envelope_strict :=
    ⟨inDerivedEnvelope_amplitude, intendedGapOneFactorAmplitude_not_inQPhi⟩

What this page does not claim

The theorem does not prove that the amplitude f has any physical meaning or corresponds to a measured quantity. The theorem does not itself derive the amplitude f; it only establishes a uniqueness property for an already-defined value. The theorem does not claim that the golden-ratio field extension is the only possible way to describe the amplitude.

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: