Masses Mass Genesis T10 Run Reference Provenance Boundary Electroweak Anchor Phi

The offset's ancestry

In the Recognition Science framework's account of particle masses, a proposed continuum target for one mass value is written as phi^42 / 8, where phi is the golden ratio. The number 42 in that expression has a specific, machine-checked origin. The declaration electroweak_anchor_phi_offset_eq_fortyTwo proves that 42 equals 55 minus 13, where 55 is the certified value of the Electroweak anchor r0 and 13 is a fixed offset. This means the 42 has anchor and topology ancestry, not settlement-integer ancestry.

The distinction matters because a separate theorem, gapOne_seed_rung_eq_zero, proves that the seed pattern's rung is 0, not 42. So the numeral 42 is not a rung of the seed pattern. The framework's library, a machine-checked collection of formal theorems, records this boundary explicitly: the 42 comes from the Electroweak anchor offset, and the continuum target phi^42/8 already lies in the permitted field Q(phi), as proved by continuumReferenceLoad_inQPhi.

What the declaration does not claim is just as important. It does not derive the run-reference functional itself, and it does not prove that such a derivation is impossible. The remaining question is one of provenance, not extension: a constant functional returning the target exists trivially, so only the ancestry of a candidate can decide the campaign. The theorem factorization_and_phiField_do_not_exclude_target shows that factorization through any killed run summary plus phi-field valuedness cannot prove the requested exclusion. The underivability floor is not expressible by these extensional properties.

/-- The numeral 42 is the Electroweak anchor offset 55 - 13. -/
theorem electroweak_anchor_phi_offset_eq_fortyTwo :
    Anchor.r0 Anchor.Sector.Electroweak - 13 = (42 : ℤ) := by
  rw [YardstickPremiseFreeCert.r0_ew_certified_eq_55]
  norm_num

/-- The manager's proposed "rung 42" is not the seed rung. -/
theorem gapOne_seed_rung_eq_zero :
    rungOf (worldlinePattern gapOneTwoPhaseMode) = 0 := by
  simp [rungOf, rungFromTopology, worldlinePattern]

/-- The squared continuum target already belongs to the permitted φ-field. -/
theorem continuumReferenceLoad_inQPhi :
    InQPhi continuumReferenceLoad := by
  unfold continuumReferenceLoad
  exact (inQPhi_phi_pow 42).div
    ⟨(8 : ℚ), (0 : ℚ), by norm_num⟩
    (by norm_num)

/-- Consequently, factorization through any killed run summary plus φ-field
valuedness cannot prove the requested W6 value exclusion. -/
theorem factorization_and_phiField_do_not_exclude_target
    {α : Type*}
    (summary : Q3SettledLedgerOctave → α) :
    ¬ (∀ f : ExactRunFunctional,
      FactorsThrough summary f →
      PhiFieldValued f →
      ∀ octave, f octave ≠ continuumReferenceLoad) := by
  intro h
  have hfac : FactorsThrough summary constantContinuumReference :=
    ⟨fun _ => continuumReferenceLoad, fun _ => rfl⟩
  have hfield : PhiFieldValued constantContinuumReference := by
    intro octave
    simpa [constantContinuumReference] using
      continuumReferenceLoad_inQPhi
  exact
    (h constantContinuumReference hfac hfield
      canonicalQ3SettledLedgerOctave) rfl

What this page does not claim

No derivation of a run-reference functional is given, and no proof that one is impossible. The numeral 42 is not a rung of the seed pattern. The constant functional returning the target is a counterexample only, not an adopted physical 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/T10RunReferenceProvenanceBoundary.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: