Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.RecognitionMeshHingeKappa4D

show as:
view Lean formalization →

Defines the mesh hinge coupling constant as unit coupling in the banked concrete-stationarity-bridge pattern for 4D recognition mesh gravity. No ratio variable and no real logarithm appear. Gravity analysts closing Wave B residual R2 cite it. The module pins kappa to 1, proves positivity and source-domination bounds, and discharges the typed residual that identifies hinge kappa.

claimOn the 4D recognition mesh, the hinge coupling $\kappa_{\mathrm{hinge}}$ equals $1$. The geometric deficit is bounded by $|\delta|\le 2\pi$, hinge channel count and mesh scale are positive, and the residual asserting that hinge $\kappa$ is identified is closed under the unit-coupling stationarity bridge (no $x$-ratio, no $\log$).

background

This module sits in the QG full-completion Wave B attack on typed residuals for 4D continuum closure. Upstream, the exact-$J$ bridge builds the canonical recognition mesh carrier on the periodic Freudenthal 4-torus and attaches a value-level action whose amplitude Hessian is the Option-C midpoint Bloch symbol. The geometric-deficit module (Wave B R1) already identifies mesh geometric deficit without an $x$-ratio. The Regge 4D star-kernel supplies the periodic-lattice star deficit class on the Freudenthal incidence layer and 15-class stencil.

Hinge coupling here is the constitutive factor that multiplies deficit into source response at a mesh hinge. The design choice is unit coupling of the banked concrete-stationarity-bridge pattern: $\kappa=1$, with no auxiliary ratio field and no real logarithm. Supporting quantities are hinge channel count, mesh scale, and absolute bounds on arcsin and geometric deficit needed to keep the residual well-typed.

proof idea

Definition layer first: mesh hinge kappa is set to the unit constant; channel count and mesh scale are positive constants of the mesh. Elementary real analysis gives $|\arcsin|\le\pi/2$ and $|\mathrm{meshGeometricDeficit}|\le 2\pi$. From unit kappa one obtains kappa equals one, kappa nonzero, and the source-dominated inequality that compares coupling strength to the deficit bound. The typed residual "hinge kappa identified" is then inhabited by packaging those facts, and a closure lemma records that the residual is discharged. No deep spectral argument: algebraic identification plus bound lemmas.

why it matters in Recognition Science

Wave B residual R2 in the QG residual DAG. Downstream, DualEntryCoupling4D assembles banked R1 (mesh geometric deficit), R2 (this hinge kappa plus source-domination), and R3 (dual-entry strain state) into an inhabited deficit-source constitutive coupling. The companion audit module requires the closure theorem and decoys to print only under propext, Classical.choice, and Quot.sound. In the broader recognition gravity stack this is the constitutive hinge link between geometric deficit on the Freudenthal mesh and source response, keeping the continuum-closure path free of ratio and log scaffolding.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (19)