module module moderate

`IndisputableMonolith.Verification.Item8ClosureTarget`

Verification module that packages the Item 8 closure target: residual signatures for lepton and quark ratio families, the coefficient data that drive predicted residuals on the φ-ladder, and the consistency claim that equal signatures force equal residual predictions. A verifier cites it when checking that family-ratio residuals are signature-determined rather than ad hoc. The module is mostly definitions plus short algebraic consistency lemmas over those signatures.

claimItem 8 closure data: a sign class from $\mathrm{sign}(B_{\mathrm{pow}})$, residual signatures and pairs for the lepton, up-quark, and down-quark ratio families, coefficient records for each family, the map from signature to predicted residual, and the target statement that equal residual signatures yield equal predicted residuals (with a consistency check on the ratio-family data).

background

Recognition Science places particle masses on a $\varphi$-ladder (yardstick times $\varphi$ to a rung offset by a gap). Ratio families compare masses within a generation sector; residuals measure how far observed ratios sit from the pure ladder prediction. The module imports the RS constants layer (including the fine-structure band) and the running-couplings development, where the anchor scale $\mu^*=182.201,\mathrm{GeV}$ is a stationarity point of the RG flow and $\beta(g)=(1/\ln\varphi),dg/dr$ is the ladder derivative of the coupling.

Locally, a sign class is induced by the sign of the power $B_{\mathrm{pow}}$. Residual signatures package that sign data with family labels; coefficient records store the numerical ladder inputs for leptons and for up- and down-type quarks. Predicted residuals are the pure functions of those signatures and coefficients. The closure target is the statement that the residual map is well-defined on signature classes.

proof idea

Definition-heavy module, not a single deep proof. It introduces the sign class, residual signature and pair types, per-family coefficient records, and the concrete lepton, up-quark, and down-quark signatures. From those it builds the ratio-family table and the predicted-residual map. The main mathematical content is a short equality lemma: identical residual signatures imply identical predicted residuals, plus a consistency check that the assembled ratio-family data hang together. No long tactic scripts; the argument is by unfolding the signature constructors and comparing coefficients.

why it matters in Recognition Science

Item 8 is a verification checkpoint: family-ratio residuals must be forced by a discrete signature (including the $B_{\mathrm{pow}}$ sign) rather than free parameters. This module names that checkpoint as an explicit closure target and supplies the supporting data types and the same-signature-same-prediction lemma. It sits downstream of the constants and $\alpha$ layers and of the $\varphi$-ladder running-coupling story (anchor scale and ladder $\beta$-function). No further modules currently depend on it in the graph, so it is a leaf verification artifact: the place a referee looks to see what "Item 8 closed" means in Lean. It does not itself prove the full mass spectrum; it only locks the residual-signature contract those spectrum claims must satisfy.

scope and limits

Does not prove experimental mass ratios; only defines residual signatures and prediction equality.
Does not derive $B_{\mathrm{pow}}$ or the $\varphi$-ladder rungs; those are imported inputs.
Does not close the full RS verification suite; only the Item 8 residual-signature target.
Does not establish RG running or the $\mu^*$ anchor; it only imports that layer.
Does not claim uniqueness of coefficient choices beyond the stated consistency lemma.

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