discrete_continuous_duality

formal source

 233    μ→τ: contribution = (face count) / (discrete measure) = F/V = 3/2
 234
 235    The vertex count V is the "discrete solid angle" for faces. -/
 236theorem discrete_continuous_duality :
 237    -- e→μ uses 1/(continuous measure)
 238    eMuContribution = 1 / (4 * Real.pi) ∧
 239    -- μ→τ uses F/(discrete measure)
 240    muTauContribution = (6 : ℝ) / 4 ∧
 241    -- The discrete measure is the vertex count
 242    discreteMeasure2DFace = 4 := by
 243  constructor
 244  · rfl
 245  constructor
 246  · unfold muTauContribution discreteMeasure2DFace faceCount faceVertexCount
 247    norm_num
 248  · rfl
 249
 250/-! ## Why Vertices Specifically?
 251
 252The vertex count is forced as the normalization factor because:
 253
 2541. **Discrete lattice**: The RS ledger is Z³, not continuous R³.
 2552. **Anchoring**: A face's contribution must be localized to lattice points.
 2563. **Vertices as anchors**: The vertices of a face are exactly the
 257   lattice points that define that face.
 2584. **Uniform distribution**: Each vertex receives 1/V of the face's
 259   total contribution (by symmetry).
 260
 261The vertex count is the unique natural normalization for a discrete
 262face on a discrete lattice.
 263-/
 264
 265/-- The number of vertices equals the number of lattice anchor points
 266    for a 2D face. (This is definitional in the discrete setting.) -/