Recog Spec Observable Payloads

Structured observable records

In physics, a prediction is only as good as the numbers that carry it. The recognition framework, which models reality as a discrete record of events, produces dimensionless ratios for particle properties. The Observable Payloads module gives those ratios a fixed, named shape. It defines two structures: LeptonMassRatios, holding mu_over_e, tau_over_e, and tau_over_mu, and CkmMixingAngles, holding vus, vcb, and vub. Each field is a real number, and each structure has a canonical order for its list view.

The point is to remove ambiguity. Earlier code stored these values as raw lists of real numbers, where position alone decided meaning. A list [a, b, c] could mean anything. Now the meaning is in the field name. The module proves that converting a record to its list and back is lossless: if two records have the same list, they are the same record. It also proves a predicate holds for the whole record exactly when it holds for every element of the list. These are small, machine-checked facts, but they make the records safe to use as the output of the framework's calculations.

In Recognition Science, this is the typed interface between the forcing chain, which derives constants and masses, and the experimental comparisons that check them. The module itself does not derive any physical value. It establishes the data format. A reader can now say precisely which ratio is meant when the framework reports a lepton mass ratio or a CKM mixing angle, and can trust that the record's structure is internally consistent.

/-- Lepton-sector inter-generation mass ratios (dimensionless). -/
structure LeptonMassRatios where
  mu_over_e   : ℝ
  tau_over_e  : ℝ
  tau_over_mu : ℝ

/-- CKM mixing-angle magnitudes (dimensionless). -/
structure CkmMixingAngles where
  vus : ℝ
  vcb : ℝ
  vub : ℝ

theorem toList_injective {a b : LeptonMassRatios} (h : a.toList = b.toList) : a = b := by
  simp only [toList] at h
  have h1 : a.mu_over_e = b.mu_over_e := List.cons.inj h |>.1
  have h23 := List.cons.inj h |>.2
  have h2 : a.tau_over_e = b.tau_over_e := List.cons.inj h23 |>.1
  have h3 : a.tau_over_mu = b.tau_over_mu := List.cons.inj (List.cons.inj h23 |>.2) |>.1
  exact ext h1 h2 h3

theorem forall_iff_list (P : ℝ → Prop) (m : LeptonMassRatios) :
    m.Forall P ↔ ∀ r ∈ m.toList, P r := by
  simp only [Forall, toList, List.mem_cons, List.mem_nil_iff, or_false]
  constructor
  · rintro ⟨h1, h2, h3⟩ r (rfl | rfl | rfl) <;> assumption
  · intro h
    exact ⟨h _ (Or.inl rfl), h _ (Or.inr (Or.inl rfl)), h _ (Or.inr (Or.inr rfl))⟩

What this page does not claim

This module does not derive any physical constant or mass ratio. This module does not define what a recognition event is. This module does not compare its records against measured particle data.

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/RecogSpec/ObservablePayloads.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: