module module moderate

`IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation`

This module supplies the D=3 specializations of hypercube face counts and the resulting structural deltas for the tau lepton generation step. Researchers constructing lepton masses on the phi-ladder would cite these identities to fix the tau coefficient. The module consists of direct algebraic definitions and equalities that follow from the base relation F = 2D.

claim$F = 2D$ for the face count of the D-hypercube. For D = 3 the structural delta satisfies $deltaStructural_{D3} = 1/2$ with the additive form $deltaAxisAdditive_{D3}$ obtained by direct substitution into the tau step coefficient.

background

Recognition Science fixes D = 3 via the eight-tick octave (T7-T8) and places lepton generations on the phi-ladder with mass steps governed by the tau coefficient (W + D/2). The module imports the time quantum tau_0 = 1 tick from Constants, the 4 pi derivation via vertex deficits of Q_3 from AlphaDerivation, and the uniqueness of the tau coefficient from TauStepExclusivity. It introduces faceCount as the hypercube face count F = 2D together with the D = 3 variants deltaStructural_D3, deltaAxisAdditive_D3 and delta_D3_derived.

proof idea

This is a definition module, no proofs. The listed siblings are obtained by direct substitution of D = 3 into the face-count identity and the structural delta expressions already established in the imported TauStepExclusivity module.

why it matters in Recognition Science

The D = 3 identities complete the structural half of the tau step delta derivation begun in TauStepExclusivity and supply the concrete coefficients needed for the lepton mass formula. They sit downstream of the alpha derivation via the cubic ledger and upstream of any numerical mass-ladder calculations.

scope and limits

Does not compute the numerical tau mass.
Does not treat electron or muon steps.
Does not incorporate loop corrections or running couplings.
Does not address non-cubic lattices.

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