IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance
Separates the physical finite-difference Dirichlet operator on the six-tetrahedron cubic lattice from the abstract canonical graph Dirichlet energy. Supplies named action and target objects that Track 1.B-PHY residual theorems and axis-stencil certificates import. Wires periodic Freudenthal geometry and cubic-lattice Regge limits into Dirichlet targets pending replacement by the explicit six-tet stencil expression.
claimOn the periodic six-tetrahedron cubic Freudenthal lattice, the module defines the physical finite-difference Dirichlet action $S_{\mathrm{FD}}$ and its target, the periodic edge-stencil Dirichlet action, and records that the canonical Hessian of the encoded triangulation coincides with the graph Dirichlet energy (no self-loops).
background
Recognition Gravity bridges discrete Regge calculus to continuum Einstein–Hilbert via a weak-field quadratic identification with the J-cost / Dirichlet energy. The nonlinear correspondence module states only a local target: near a flat configuration the full nonlinear Regge action equals its flat value plus the canonical J/Dirichlet quadratic, without claiming global exact equality.
The periodic Freudenthal torus supplies the scalable typed vertex/edge/tetrahedron model and the incidence edge-slot partition needed by the first-variation theorem. The cubic-lattice limit module isolates the regular weak-field $O(a^2)$ case of the second-order Regge action from the general CMS curvature-measure statement. Length-chain Schläfli certificates give closed-form dihedral derivatives on the Freudenthal tet edge set.
This module sits between those geometry inputs and the physical residual track: it names the finite-difference Dirichlet operator as a distinct object from the abstract graph energy so later stencil algebra can replace the placeholder.
proof idea
Definition and certificate assembly, not a single end-to-end theorem. It introduces physical finite-difference Dirichlet action/target abbreviations, periodic edge-stencil and mixed-axis stencil actions, and nonnegativity or no-self-loop lemmas that discharge the Dirichlet-target interface. Canonical-Hessian-is-Dirichlet facts are obtained from the encoded periodic Freudenthal triangulation. The doc-comment flags the six-tet cubic stencil body as still to be substituted for the placeholder.
why it matters in Recognition Science
Track 1.B-PHY packages the physical finite-probe Regge-to-EH residual theorems from this module as a structural upgrade beyond the flat-substrate witness. MasterTheoremHandoffIntegration lists the physical residual and Bianchi interface among the fork handoffs. FreudenthalAxisStencilCoeffCert audits corrected axis-stencil monomial coefficients against the same lattice residual. ReggeTTSymbolPreflight uses the true nonlinear action and flat-point identification in the TT Bloch-symbol program. UnifiedForcingChain imports the gravity stack as part of the T0–T8 forcing surface. The module therefore is the named physical Dirichlet instance that keeps abstract graph energy separate from the six-tet cubic stencil until the latter is filled in.
scope and limits
- Does not yet contain the actual six-tet cubic stencil expression; that remains a placeholder.
- Does not claim global equality of full nonlinear Regge action with summed J-cost.
- Does not enumerate a concrete finite n×m×k mesh; uses the typed periodic model only.
- Does not prove continuum EH convergence beyond the cubic-lattice O(a²) special case imported upstream.
- Does not certify floating-point numerics; downstream coeff certs are exact-rational.
used by (5)
depends on (4)
declarations in this module (597)
-
def
CanonicalHessianIsDirichlet -
theorem
canonicalHessianIsDirichlet_of_encodedPeriodicFreudenthal -
abbrev
PhysicalFiniteDifferenceDirichletAction -
def
PhysicalFiniteDifferenceDirichletTarget -
def
periodicEdgeStencilDirichletAction -
def
periodicAxisDisp -
def
canonicalPeriodicMixedAxisStencilAction -
def
PeriodicEdgeStencilDirichletTarget -
theorem
periodicEdgeStencilDirichletAction_nonneg -
theorem
periodicEdgeStencilTarget_of_noSelfLoop -
theorem
canonicalPeriodicNoSelfLoopEdges -
theorem
canonicalPeriodicEdgeStencilTarget -
theorem
canonicalPeriodicJQuadraticTerm_eq_edgeStencil -
def
CanonicalPeriodicEdgeStencilLocalCorrespondence -
def
CanonicalPeriodicStrongestTrueReplacement -
theorem
canonicalPeriodicStrongestTrueReplacement_iff_edgeStencilLocalCorrespondence -
theorem
canonicalPeriodicEdgeStencilLocalCorrespondence_of_taylor -
theorem
canonicalPeriodicEdgeStencilLocalCorrespondence_of_flat_and_remainderJets -
theorem
supplies -
theorem
canonicalPeriodicEdgeStencilLocalCorrespondence_of_flat_first_and_directionalHessian -
theorem
canonicalPeriodicEdgeStencilLocalCorrespondence_of_eventuallyZero_edgeStencil_and_taylor -
theorem
canonicalPeriodicEdgeStencilLocalCorrespondence_of_localHessianTaylorInputs -
theorem
canonicalPeriodicStrongestTrueReplacement_of_localHessianTaylorInputs -
structure
PeriodicFreudenthalDirichletCertificate -
def
regularModel_of_periodicFreudenthalCertificate -
def
physicalSixTetModel_of_periodicFreudenthalCertificate -
def
cubicLimitInput_of_periodicFreudenthalCertificate -
theorem
periodicFreudenthalCertificate_cubicLimit -
theorem
periodicFreudenthalCertificate_error_vanishes_along_family -
theorem
periodicFreudenthalCertificate_error_vanishes_of_bounded_error_and_spacing -
structure
PeriodicFreudenthalRefinementFamily -
def
exactPeriodicFreudenthalComparisonCertificate -
def
exactPeriodicFreudenthalComparisonCertificateAtSpacing -
theorem
exactPeriodicFreudenthalComparisonCertificateAtSpacing_converges -
def
canonicalPeriodicEdgeStencilComparisonCertificate -
def
canonicalPeriodicEdgeStencilComparisonCertificateAtSpacing -
def
canonicalPeriodicEdgeStencilContinuumCertificateAtSpacing -
theorem
canonicalPeriodicEdgeStencilComparisonCertificateAtSpacing_converges -
def
canonicalPeriodicEdgeStencilRefinementFamily -
theorem
canonicalPeriodicEdgeStencilRefinementFamily_pointwise_converges -
def
canonicalPeriodicEdgeStencilContinuumRefinementFamily -
theorem
canonicalPeriodicEdgeStencilContinuumRefinementFamily_pointwise_converges -
theorem
canonicalPeriodicEdgeStencilContinuumRefinementFamily_converges_to_fixed_limit -
structure
CanonicalPeriodicFixedContinuumComparisonData -
abbrev
CanonicalPeriodicFixedPhysicalContinuumAction -
structure
CanonicalPeriodicFixedPhysicalActionComparisonData -
def
canonicalPeriodicFixedDirichletContinuumAction -
theorem
canonicalPeriodicFixedDirichletContinuumAction_eq_reggeSecondOrder -
def
canonicalPeriodicFixedDirichletActionComparisonData -
theorem
canonicalPeriodicFixedDirichletAction_pointwise_tendsto -
theorem
canonicalPeriodicFixedDirichletAction_weighted_finite_probe_residual_tendsto_zero -
theorem
canonicalPeriodicFixedDirichletAction_variable_weighted_finite_probe_residual_tendsto_zero -
theorem
canonicalPeriodicNonlinearResidual_bound_to_fixedDirichlet -
theorem
canonicalPeriodicNonlinearResidual_tendsto_zero_to_fixedDirichlet -
theorem
canonicalPeriodicNonlinearResidual_tendsto_zero_eventually_to_fixedDirichlet -
theorem
canonicalPeriodicNonlinearResidual_tendsto_zero_scaled_to_fixedDirichlet -
theorem
canonicalPeriodicNonlinearResidual_tendsto_zero_spacing_scaled_to_fixedDirichlet -
theorem
canonicalPeriodicNonlinearResidual_weighted_finite_probe_spacing_scaled_tendsto_zero -
theorem
canonicalPeriodicNonlinearResidual_variable_weighted_finite_probe_spacing_scaled_tendsto_zero -
theorem
canonicalPeriodicNonlinearResidual_variable_weighted_finite_probe_spacing_scaled_to_secondOrder_tendsto_zero -
theorem
canonicalPeriodicNonlinearAggregate_variable_weighted_finite_probe_spacing_scaled_to_secondOrder_residual_tendsto_zero -
theorem
canonicalPeriodicNonlinearResidual_variable_weighted_finite_probe_spacing_scaled_to_secondOrder_div_spacing_norm_sq_tendsto_zero -
theorem
canonicalPeriodicSecondOrder_variable_weighted_finite_probe_spacing_scaled_div_spacing_norm_sq_tendsto -
def
FlatDeficitZeroTarget -
def
FlatDeficitAngleSumTarget -
theorem
flatDeficitZeroTarget_of_angleSum -
theorem
flatDeficitZeroTarget_iff_globalZeroDeficitAtFlat -
theorem
globalZeroDeficitAtFlat_of_angleSum -
def
freudenthalLocalDihedralAngle -
def
canonicalPeriodicTypedEdgeAngleContribution -
def
CanonicalPeriodicTypedEdgeAngleSumTarget -
def
CanonicalPeriodicDirectTypedEdgeAngleSumTarget -
def
canonicalPeriodicTypedEdgeIncident -
instance
canonicalPeriodicTypedEdgeIncident_decidable -
def
canonicalPeriodicTypedEdgeIncidentSlotWitness -
instance
canonicalPeriodicTypedEdgeIncidentSlotWitness_decidable -
theorem
canonicalPeriodicTypedEdgeIncident_iff_slotWitness -
theorem
canonicalPeriodicTypedEdge_eq_localEdgeOf_of_slotWitness -
theorem
canonicalPeriodicTypedEdgeAngleContribution_eq_of_slot -
def
canonicalPeriodicTypedEdgeLocalEdgeOfWitness