module module high

`IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation`

The module derives the structural and axis-additive deltas for the tau lepton generation step at D=3 by applying the face-count identity of the hypercube. Researchers modeling RS-native lepton mass ladders would cite the explicit D=3 formulas for the correction terms. The argument reduces to algebraic substitution of F=2D into the general expressions after importing the exclusivity coefficient from the upstream module.

claim$F = 2D$ for the face count of the $D$-hypercube, which yields the explicit structural delta and axis-additive delta for the tau step at $D=3$.

background

Recognition Science obtains lepton generation steps from the geometry of the cubic ledger. The module imports the RS time quantum from Constants and the alpha derivation via Gauss-Bonnet on vertex deficits of $Q_3$. It builds on the TauStepExclusivity result that forces the coefficient $(W + D/2)$ for admissible dimension-dependent corrections in the tau step.

proof idea

The module defines faceCount, faceVertexCount and their D=3 specializations, then derives deltaStructural_D3, deltaAxisAdditive_D3 and delta_D3_derived by direct substitution of D=3 into the structural formulas. All steps are algebraic identities using the imported exclusivity result.

why it matters in Recognition Science

This module supplies the concrete D=3 expressions for the tau step delta that close the lepton generation chain. It realizes the T8 forcing of D=3 and supplies the gap correction needed for the phi-ladder mass formula. It extends the exclusivity result from TauStepExclusivity to explicit numerical corrections.

scope and limits

Does not derive the general-D face count from first principles.
Does not compute the numerical tau mass value.
Does not address the electron or muon generation steps.
Does not incorporate loop corrections beyond the structural delta.

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