pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Ablation

show as:
view Lean formalization →

The Ablation module supplies definitions to remove the +4 offset from Z when handling quarks on the Recognition Science mass ladder. Researchers computing quark masses or Z-gap adjustments cite these to eliminate an empirical correction. The module organizes its content around drop functions, equality lemmas, and contradiction checks with no core proofs.

claimThe module defines $Z_{drop+4}$, $Z_{dropQ4}$, and $Z_{break6Q}$ that remove the $+4$ offset for quarks, together with the anchor equality $AnchorEq$ implying $Z_{eq} non-negative$.

background

Recognition Science inserts Z as the gap parameter in the mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder. The Ablation module works inside the quark sector to drop the +4 offset, introducing the listed sibling declarations. This setting rests on the J-cost and defectDist conventions imported from the foundation modules.

proof idea

This is a definition module, no proofs. It collects the offset-removal declarations and supporting equalities in one place.

why it matters in Recognition Science

The module supplies clean Z values for quarks that feed into parent mass-formula theorems and the phi-ladder calculations. It closes the empirical +4 adjustment noted in the module documentation.

scope and limits

declarations in this module (6)