module module moderate

`IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation`

The TauStepDeltaDerivation module assembles the structural delta for the tau lepton generation step in D=3 from the D-hypercube face count. Physicists deriving lepton mass hierarchies on the phi-ladder would cite it to obtain the concrete D=3 correction. The module combines the imported exclusivity constraint on (W + D/2) with the geometric identity F = 2D.

claimThe face count of the D-hypercube is $F = 2D$. This identity yields the structural delta $\\delta_{D3}$ for the tau generation step once the coefficient $(W + D/2)$ is fixed by the exclusivity result.

background

The module sits inside the lepton generations section and imports the RS time quantum $\tau_0 = 1$ tick, the alpha derivation from vertex deficits of the cubic ledger, and the tau step exclusivity theorem. The central definition is the face count $F = 2D$ of the D-hypercube, which supplies the additive correction entering the defectDist and phi-ladder mass formulas.

The local setting is the eight-tick octave and D = 3 forced by the unified forcing chain. The imported TauStepExclusivity result states that the coefficient (W + D/2) is the unique admissible dimension-dependent correction for the tau step.

proof idea

This is a definition module, no proofs. It defines faceCount, deltaStructural_D3, deltaAxisAdditive_D3 and the derived quantities by direct substitution of F = 2D into the structural and axis-additive expressions, then specializes to D = 3.

why it matters in Recognition Science

The module supplies the concrete $\delta_{D3}$ required to close the tau step in the lepton generation chain and to fix the tau rung on the phi-ladder. It feeds the mass formula that uses yardstick $\times \phi^{rung-8+gap(Z)}$ and connects the hypercube geometry to the (W + D/2) coefficient established in TauStepExclusivity.

scope and limits

Does not prove the exclusivity of the (W + D/2) coefficient.
Does not compute numerical lepton masses or rungs.
Does not address the electron or muon generation steps.
Does not extend the face-count identity beyond the D-hypercube.
Does not derive alpha or other constants from first principles.

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