module module moderate

`IndisputableMonolith.Verification.Item8ClosureTarget`

Verification module for Item 8 closure: residual signatures of lepton and quark mass ratios on the φ-ladder. It packages sign classes from B-power, family coefficient data, and predicted residual pairs, then proves that equal signatures yield equal predictions and that the ratio-family map is internally consistent. Cite when auditing mass-ladder residual checks against running-coupling anchors.

claimItem 8 closure target: residual signatures $S$ for leptons, up-type quarks, and down-type quarks, built from the sign of $B_{\mathrm{pow}}$ and ratio-family coefficients; predicted residuals $R(S)$; if $S_1=S_2$ then $R(S_1)=R(S_2)$; and consistency of the ratio-family assignment.

background

Recognition Science places particle masses on a φ-ladder with yardstick and rung offsets. Residual checks compare observed mass ratios to ladder predictions after accounting for running couplings. The RS anchor scale μ* ≈ 182.2 GeV is a stationarity point of the RG flow; β-function structure is the ladder derivative β(g) = (1/ln φ) dg/dr.

This module sits in the Verification domain. It imports native constants (including the fine-structure band machinery) and the running-couplings layer. Local objects classify the sign induced by B_pow, package residual pairs, and attach coefficient data to lepton, up-quark, and down-quark families so that Item 8 can be stated as a closed, checkable target rather than an ad hoc table.

proof idea

Definition-heavy module with thin equational theorems. Sign classes, residual signatures, residual pairs, and ratio-family coefficients are introduced as data. Family-specific signatures (lepton, up, down) and the ratio-family map feed a predicted-residuals construction. The main lemmas are functional: identical signatures imply identical predictions, and the ratio-family assignment is consistent with those predictions. No deep analytic argument; structure is by construction plus equality rewriting.

why it matters in Recognition Science

Item 8 is the residual-signature closure step in the RS verification checklist: mass-ratio residuals for the three charged families must match the φ-ladder prediction once B_pow signs and family coefficients are fixed. Downstream consumers are external to this file (no in-repo used_by edges), but the named target item8ClosureTarget and the consistency lemma are the objects a full audit would discharge against experimental ratios and the α band. Ties to the mass formula (yardstick · φ^(rung−8+gap(Z))) and to running couplings at the RS anchor, without reopening T5–T8 forcing.

scope and limits

Does not derive B_pow or family coefficients from the forcing chain T0–T8.
Does not prove numerical agreement with PDG masses; only signature-to-prediction consistency.
Does not establish RG flow or β-function identities; those live in RunningCouplings.
Does not bound α^{-1} or fix G, ħ; constants are imported, not re-proved.
Does not claim completeness of the three-family list beyond the packaged signatures.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Physics.RunningCouplings module_import

declarations in this module (102)

inductive BpowSign L99
structure ResidualSignature L105
structure ResidualPair L114
structure RatioFamilyCoeffs L120
def leptonSignature L125
def upQuarkSignature L134
def downQuarkSignature L143
def ratioFamily L160
def predictedResiduals L172
theorem same_signature_same_prediction L178
def item8ClosureTarget L194
theorem consistency_of_ratioFamily L219
theorem consistency_necessary L235
structure RefinedCoeffs L257
def refinedFamily L262
def refinedPrediction L276
theorem refined_at_eta_zero L281
def refinedItem8ClosureTarget L286
def etaFromData L335
theorem etaL_gen12_identity L341
theorem etaL_gen23_identity L352
theorem eta_absorbs_consistency L365
theorem refinedFamily_neg_solvable L379
theorem refinedFamily_pos_solvable L417
theorem refinedFamily_neg_unique L460
theorem refinedFamily_pos_unique L515
theorem neg_cPos_irrelevant L564
theorem pos_cNeg_irrelevant L571
theorem refined_neg_sector_closure L584
structure SignClassCoeffs L622
def signClassFamily L631
theorem signClass_collapse_to_refined L647
def pdg_up L667
def pdg_charm L668
def pdg_top L669
def pdg_down L670
def pdg_strange L671
def pdg_bottom L672
def pdg_electron L673
def pdg_muon L674
def pdg_tau L675
def alphaStrong L679
def rungResidual L683
def upGen12Residual L686
def upGen23Residual L689
def downGen12Residual L692
def downGen23Residual L695
def leptonGen12Residual L698
def leptonGen23Residual L701
def upExact L706
def downExact L712
def leptonObserved L718
def item8Specialized L727
def allSectorTest L740
def refinedItem8Specialized L752
def refinedAllSectorTest L758
def leptonEta L773
def upQuarkEta L778
def downQuarkEta L782
def kappaLeptonCandidate L799
theorem kappaLeptonCandidate_pos L801
theorem kappaLeptonCandidate_ne_zero L805
theorem leptonLogAsym_pos L809
theorem leptonLogAsym_ne_zero L813
theorem leptonGen12Residual_pos L817
theorem leptonGen12Residual_ne_zero L835
theorem leptonGen23Residual_neg L839
theorem leptonCrossDiff_pos L860
theorem leptonCrossDiff_ne_zero L864
theorem leptonSectorClosure L871
def leptonAnchoredCNeg L887
def leptonAnchoredCoeffs L893
def alphaS6At L904
def alphaSAtTopThreshold L909
def alphaS5At L913
def alphaSAtBottomThreshold L918
def alphaS4At L922
def alphaSAtCharmThreshold L927
def alphaS3At L931
def alphaSPiecewise L936

… and 22 more