pith. sign in
module module high

IndisputableMonolith.RSBridge.ZMapDerivation

show as:
view Lean formalization →

ZMapDerivation module defines the integerization scale with one channel per cube face in the cubic ledger. It supplies Z-polynomials, lepton decompositions, and equality statements that align with anchor values. Recognition theorists mapping the phi-ladder to Standard Model fermions would cite these constructions. The module consists of definitions and direct equality lemmas.

claimThe integerization scale satisfies one channel per cube face. The Z-polynomial is even with a zero at the origin; the lepton decomposition matches the anchor value via $Z_l = q̃^2 + q̃^4$.

background

The module sits in the RSBridge domain and imports AlphaDerivation together with Anchor. AlphaDerivation supplies the structural derivation of α^{-1} via 4π from Gauss-Bonnet on vertex deficits of Q₃. Anchor defines the 12 fermions, the charge-indexed integer ZOf = q̃² + q̃⁴ (+4 for quarks), the gap function F(Z) = ln(1 + Z/φ)/ln(φ), and massAtAnchor at scale μ⋆.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Z-map constructions into RSBridge.Anchor for fermion species and gap applications. It supplies the integerization step required to place recognition costs on the phi-ladder and connect to the T5–T8 forcing chain and the RCL identity.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)