recognition › ask › explain-the-lean-theorem-match-rsbridge-rung-up-quarks-in-mo-4fdc8e74

Explain the Lean theorem `match_rsbridge_rung_up_quarks` in module `IndisputableMonolith.Masses.RungConstructor.Proofs`. Write for an educated reader who knows science and programming but may not know Lean. Cover: (1) what the declaration says in plain English, (2) why it matters in Recognition Science, (3) how to read the formal statement, (4) visible dependencies or certificates in the supplied source, and (5) what this declaration does not prove. Cite only declarations present in the supplied Recognition source.

permalink: https://pith.science/recognition/ask/explain-the-lean-theorem-match-rsbridge-rung-up-quarks-in-mo-4fdc8e74 · first asked 2026-05-10 · browse all asks

confidence: high in recognition cached

The declaration match_rsbridge_rung_up_quarks asserts that the new rung constructor reproduces the legacy rung values for the three up-type quarks.

(1) In plain English: for the up quark (u), charm quark (c), and top quark (t), the rung number produced by compute_rung (.fermion .u) (and likewise for c and t) is definitionally identical to the value returned by the older RSBridge.rung function.

(2) It matters in Recognition Science because the rung numbers are the discrete exponents that determine particle masses via the phi-power scaling law; preserving the legacy values guarantees that all prior mass predictions remain unchanged when the constructor is updated.

(3) The formal statement is a conjunction of three equalities: compute_rung (.fermion .u) = RSBridge.rung .u ∧ compute_rung (.fermion .c) = RSBridge.rung .c ∧ compute_rung (.fermion .t) = RSBridge.rung .t proved by the triple ⟨rfl, rfl, rfl⟩. In Lean, rfl means each side reduces to the same term by definition, so no further proof steps are required.

(4) Visible dependencies in the supplied source: the theorem sits inside the RungConstructor.Proofs module, which imports IndisputableMonolith.Masses.RungConstructor.Motif (supplying compute_rung) and IndisputableMonolith.RSBridge.Anchor (supplying RSBridge.rung). Parallel matching theorems exist for charged leptons (match_rsbridge_rung_charged_leptons), down quarks, neutrinos, and bosons; the master theorem match_rsbridge_rung generalizes the pattern to every fermion via case analysis. SDGT variants (e.g., sdgt_up_u) are also present but are not referenced here.

(5) The declaration does not prove the origin of the rung numbers, any link to the J-cost functional equation, the phi-forcing chain, or the actual mass formula; it only certifies agreement with the legacy table.

cited recognition theorems

Proofs.match_rsbridge_rung_up_quarks The theorem whose meaning is requested; its statement and rfl proof are the direct subject.
Proofs.match_rsbridge_rung Master theorem that generalizes the up-quark case to all fermions by case analysis.
Proofs.match_rsbridge_rung_charged_leptons Parallel matching theorem for leptons, illustrating the uniform pattern used for quarks.

outside recognition

Aspects Recognition does not yet address:

Any derivation of the rung values themselves from the phi forcing chain or cost uniqueness
The explicit mass scaling formula (yardstick * phi^(rung - 8 + gap(Z)))
Physical interpretation of rungs as mass exponents or connection to the Universal Forcing thesis

recognition modules consulted

The Recognition library is at github.com/jonwashburn/shape-of-logic. The model is restricted to the supplied Lean source and instructed not to invent theorem names. Treat output as a starting point, not a verified proof.