pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

A

show as:
view Lean formalization →

A denotes the single active edge transition per fundamental tick in the Recognition Science mass constants, fixed at unity. Mass modelers cite it when building sector yardsticks B_pow and r0 from cube geometry at D=3. The declaration is a direct abbreviation of the upstream active_edges_per_tick constant.

claimLet $A$ be the number of active edges per atomic tick. Then $A=1$.

background

The Masses.Anchor module centralizes parameter-free constants derived from cube geometry in three spatial dimensions. Total edges equal 12, passive edges equal 11, wallpaper groups W equal 17, and A supplies the single active transition per tick. Upstream, active_edges_per_tick is defined as 1 by T2, while IntegrationGap.A encodes the phi-power balance identity at D=3: phi^(A - gap) * phi^gap = phi.

proof idea

One-line abbreviation that directly aliases the constant active_edges_per_tick from AlphaDerivation.

why it matters in Recognition Science

A anchors the B_pow and r0 formulas for lepton, up-quark, down-quark, and electroweak sectors. It supplies the active-edge term in downstream Noether spaceShift and timeShift, actionJ_convex_on_interp, and EnergyConservationDomainCert.applied. The constant realizes the T7 eight-tick octave and T8 D=3 step of the forcing chain.

scope and limits

formal statement (Lean)

  61abbrev A : ℕ := active_edges_per_tick

proof body

Definition body.

  62
  63/-- Coherence energy unit: `E_coh = φ⁻⁵` (dimensionless; multiply by eV externally). -/

used by (40)

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

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.