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

total_geometric_content

show as:
view Lean formalization →

The definition sums the vertex, edge, face, passive-field-edge, and wallpaper-group counts of the D-hypercube to obtain the total geometric content integer. Mass baseline calculations cite it to fix the neutrino rung offset as the negation of this sum evaluated at D = 3. It is realized as a direct arithmetic combination of five independent combinatorial definitions supplied by the AlphaDerivation module.

claimLet $V(D) = 2^D$, $E(D) = D · 2^{D-1}$, $F(D) = 2D$, $P(D) = E(D) - a$ (with $a$ the active edges per tick), and $W = 17$ the number of wallpaper groups. The total geometric content of the D-hypercube is the integer $V(D) + E(D) + F(D) + P(D) + W$.

background

This module upgrades several boundary assumptions in the Recognition Science mass ladder to derived status by tracing them to the combinatorics of the 3-cube at D = 3. The total geometric content aggregates the standard hypercube counts together with passive field edges and the crystallographic constant of 17 wallpaper groups. Every integer here traces to the single input D = 3 via the cube-geometric functions listed in the module table (B-13 neutrino baseline among them).

proof idea

The definition is a one-line arithmetic sum that directly invokes the five upstream combinatorial functions: cube_vertices, cube_edges, cube_faces, passive_field_edges, and wallpaper_groups.

why it matters in Recognition Science

This definition supplies the integer 54 that appears in the neutrino baseline derivation (B-13). It is used by the theorem total_geometric_at_D3, which evaluates the sum at D = 3, and by neutrino_baseline_int, which negates the result to obtain the rung offset. In the framework it closes the derivation of the neutrino baseline from the single input D = 3, consistent with the eight-tick octave and spatial dimension D = 3.

scope and limits

formal statement (Lean)

 117def total_geometric_content (d : ℕ) : ℕ :=

proof body

Definition body.

 118  cube_vertices d + cube_edges d + cube_faces d +
 119  passive_field_edges d + wallpaper_groups
 120
 121/-- At D = 3: total geometric content = 8 + 12 + 6 + 11 + 17 = 54. -/

used by (2)

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

depends on (12)

Lean names referenced from this declaration's body.