module module moderate

`IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation`

The module supplies the face count of the D-hypercube and the structural delta derivations for the tau lepton generation step. It specializes hypercube geometry to D=3 after importing the tau exclusivity and alpha modules. Researchers modeling lepton mass hierarchies on the phi-ladder would cite these definitions. The module contains only definitions with no theorem proofs.

claimThe face count of a D-hypercube satisfies $F=2D$. Structural and axis-additive deltas for the tau generation step are defined for $D=3$ from this count.

background

Recognition Science fixes the time quantum at $ au_0=1$ tick. The imported alpha derivation obtains $4\pi$ from Gauss-Bonnet on vertex deficits of the cubic lattice $Q_3$. The tau step exclusivity module shows that the coefficient $W+D/2$ is the unique admissible form for the tau generation correction.

This module introduces the face count $F=2D$ of the D-hypercube and defines the structural and axis-additive delta terms specialized to three dimensions for use in the lepton generation mass steps.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the geometric delta terms required for the tau generation step in the lepton mass formula. It follows directly from the tau step exclusivity result and the alpha derivation from the cubic ledger. No downstream theorems are recorded as users of this module.

scope and limits

Does not prove uniqueness of the tau coefficient.
Does not derive the fine-structure constant.
Does not compute numerical lepton masses.
Does not treat electron or muon generations.
Does not apply the Recognition Composition Law.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity module_import

declarations in this module (34)

def faceCount L103
def faceVertexCount L106
theorem faceVertexCount_D3 L109
theorem faceCount_D3 L112
def deltaStructural L121
def deltaAxisAdditive L125
theorem deltaStructural_D3 L130
theorem deltaAxisAdditive_D3 L135
theorem delta_D3_derived L143
theorem deltaStructural_alt_D3 L159
theorem deltaStructural_eq_half_D3 L165
theorem faceVertexRatio_D3 L185
theorem D3_has_2D_faces L191
def continuousMeasure3D L208
def discreteMeasure2DFace L211
theorem discreteMeasure_eq_4 L214
def eMuContribution L218
def muTauContribution L222
theorem muTauContribution_eq L226
theorem discrete_continuous_duality L236
theorem vertices_are_anchors L267
inductive CellDim L295
def cellCount L303
def anchorsPerCell L310
def localCoeff L317
theorem localCoeff_vertex L320
theorem localCoeff_edge L324
theorem localCoeff_face L328
theorem localCoeff_cube L332
theorem localCoeff_eq_three_halves_iff L339
theorem localCoeff_face_ne_edge L377
theorem localCoeff_face_ne_cube L382
theorem edge_over_cube_vertices_eq_face_over_face_vertices L389
theorem delta_derived_not_calibrated L404