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

IndisputableMonolith.RSBridge.ZMapDerivation

show as:
view Lean formalization →

The ZMapDerivation module supplies the integerization scale that maps continuous recognition charges to discrete Z values, one channel per cube face. It defines Z_poly, minimal coefficients, and lepton decompositions while proving equalities that align with the anchor scale. The module consists of definitions plus equality lemmas that connect cubic ledger geometry to fermion ZOf. Researchers deriving masses on the phi-ladder cite it for the charge discretization step.

claimThe integerization scale assigns to each charge an integer $Z$ with one channel per cube face; $Z = q̃^2 + q̃^4$ (+4 for quarks), $Z_ poly$ is the even polynomial form, and the lepton case satisfies $Z_ lepton = Z_ anchor$.

background

The module sits in the RSBridge domain and imports the cubic ledger geometry together with the 4π derivation from vertex deficits in AlphaDerivation. It also imports the core bridge objects from Anchor: the 12 fermions, the charge-indexed $ZOf = q̃^2 + q̃^4$ (+4 for quarks), the gap function $F(Z) = ln(1 + Z/φ)/ln(φ)$, and massAtAnchor at the anchor scale μ⋆. The integerization scale is introduced as the discretization map that produces one integer channel per cube face, with supporting objects Z_poly (even polynomial), minimal_coefficients, and the lepton decomposition lemmas.

proof idea

This is a definition module whose argument proceeds by successive definitions: integerization_scale, Z_poly, minimal_coefficients, followed by equality lemmas integerization_scale_eq, Z_poly_even, Z_poly_zero, unit_coefficients_minimal, Z_lepton_eq, Z_lepton_decomposition, and the terminal match Z_lepton_matches_anchor_value.

why it matters in Recognition Science

The module supplies the Z-map bridge required by the Anchor definitions for fermion species and gap(F). It completes the integerization step that links the cubic geometry (T8, D=3) and the recognition composition law to the phi-ladder mass formula yardstick · φ^(rung-8+gap(Z)). By establishing Z_lepton_matches_anchor_value it closes the channel from recognition charges to observable lepton anchors.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)