Masses Mass Genesis T10 Run Reference Provenance Boundary Factorization And Phi

The provenance boundary

A mathematical target can be the right number for the wrong reason. In the Recognition Science account of particle masses, the continuum target phi^42/8 (the golden ratio raised to the power 42, divided by 8) is a specific real number that a proposed law should produce. The declaration factorization_and_phiField_do_not_exclude_target proves a negative boundary: no theorem of the form "every functional that factors through a killed run summary and lands in the field Q(phi) misses the target" is true. In plainer words, the target's value and its membership in a permitted field of numbers cannot, by themselves, rule out a candidate law that returns it.

The proof works by exhibiting a counterexample. The constant functional, the one that ignores its input and always returns phi^42/8, trivially factors through every run summary and is Q(phi)-valued. Since this functional exists, any claim that those two properties force a miss is false. The theorem does not say the constant functional is a physical law. The docstring marks it explicitly as a counterexample only, not an adopted law. The point is narrower: the extensional properties of a function, what it outputs and which field its outputs live in, cannot express the underivability floor the campaign sought.

What the declaration leaves open is the question of provenance. The numeral 42 in the target is not a rung of the seed pattern; a separate theorem proves the gap-one worldline seed has rung 0. Instead, 42 equals 55 minus 13, the Electroweak anchor offset. The target itself already lies in Q(phi), and it equals the intended gap-one factor amplitude squared. These are all kernel-checked facts. But no derivation of a run-reference functional is given, and no proof that one is impossible. The remaining question is ancestry, not extension: an f returning the target exists trivially, so only the provenance of a candidate can decide the campaign.

In Recognition Science, the result sharpens what a mass-genesis derivation must establish. A candidate law cannot be validated by checking its outputs alone; the framework's library shows that the value and the field are too weak to exclude anything. The campaign must instead track where the functional comes from, a provenance property that currently has no Lean predicate. The theorem does not close the campaign. It converts a hoped-for exclusion into a precise statement about what cannot be excluded, and redirects the search toward ancestry.

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

theorem constantContinuumReference_returns_target
    (octave : Q3SettledLedgerOctave) :
    constantContinuumReference octave = continuumReferenceLoad :=
  rfl

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

/-- Existing target identification; its ancestry is the topology/MassLaw chain. -/
theorem continuumReferenceLoad_eq_intendedSquare :
    continuumReferenceLoad = intendedGapOneFactorAmplitude ^ 2 := by
  simpa [continuumReferenceLoad, intendedGapOneFactorAmplitude] using
    gapOne_factorAmplitude_sq_eq_phi42_div_eight.symm

What this page does not claim

The constant functional is not claimed to be a physical law; it is a counterexample only. No derivation of a run-reference functional is claimed to exist. No proof that a run-reference functional is impossible is claimed.

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: