Pith. sign in
module module moderate

IndisputableMonolith.Physics.AnchorPolicy

show as:
view Lean formalization →

Policy layer for the Recognition Science mass anchor: log-φ, the display F, canonical Z-bands for light fermions, and the residue f at the structural scale μ⋆. Downstream non-circularity certificates cite it to show μ⋆ is fixed by PMS/BLM stationarity, not by mass inputs. Content is mostly definitions and equalities linking the gap function to RG-transported residues.

claimAnchor policy package: $\ln\phi$; display $F(Z)=\ln(1+Z/\phi)/\ln\phi$ identified with the gap; a canonical anchor scale $\mu_\star$ with Z-bands for the electron and light quarks; residue $f$ at that scale; and stationarity plus a stability bound of the residue at the anchor.

background

Recognition Science places fermion masses on a φ-ladder at an anchor scale μ⋆. The bridge module supplies the twelve SM fermions, the charge-indexed integers Z_i, the gap (display) F(Z)=ln(1+Z/φ)/ln(φ), and mass-at-anchor. In RS-native units the golden ratio φ is forced by the self-similar fixed point (T6).

Empirical comparison needs a residue after RG running. The RG-transport module defines the empirical mass residue f^exp by transporting SM running masses to μ⋆. This policy module sits between those two layers: it freezes the concrete anchor choice, the light-fermion Z-bands, and the residue evaluation used in certificates.

Constants supply the RS time quantum and φ-derived units. The policy does not re-derive the forcing chain; it only names the anchor data those certificates will treat as structural rather than fitted.

proof idea

Definition and specification module, not a deep proof development. It introduces ln φ, the display F and its equality with the bridge gap, an AnchorSpec record, the canonical anchor and Z-bands (electron, up, down), the residue f, and two named properties: stationarity of the residue at the anchor and a stability bound there. Equalities are short algebraic or definitional unfolds against the bridge and RG-transport imports; no substantial tactic scripts are required for the module's role.

why it matters in Recognition Science

Feeds the Anchor Non-Circularity Certificate, which claims μ⋆ ≃ 182.201 GeV is fixed by PMS/BLM stationarity independent of fermion mass inputs. That certificate imports this policy so the anchor, Z-bands, and residue are a single named object rather than ad hoc locals.

In the broader framework the gap F and φ-ladder mass formula (yardstick · φ^(rung−8+gap(Z))) are the bridge from recognition cost to particle masses. Pinning the anchor policy here keeps the non-circularity argument honest: stationarity and stability are stated on the same F and f that mass predictions use, without smuggling measured masses into μ⋆.

Without this module the verification layer would re-specify Z-bands and residue conventions in every certificate, risking silent drift from the physics bridge.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (19)