Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D

show as:
view Lean formalization →

Defines the R3 dual-entry enrichment of a bare recognition ledger: integer debit/credit columns, nonnegative magnitude, unit flux, with strain equal to the signed product (debit − credit)·mag. Supplies the discrete carrier, enriched witnesses, and bare-projection lemmas that close the missing deficit-source constitutive coupling. Gravity analysts cite it when assembling mesh dual-entry couplings or auditing Wave B residuals. The module is largely definitional with short algebraic identities and non-injectivity facts.

claimA dual-entry strain state is a 4-tuple $(d,c,m,f)$ of integer debit and credit columns, nonnegative magnitude $m$, and unit flux $f$, with strain $\sigma=(d-c)\cdot m$. The enrichment builds a recognition ledger from such states without using ratio fields or real logarithms, and projects back to a bare ledger that is not injective on the enriched data.

background

Recognition Science gravity work treats the ledger as the discrete substrate of geometry. Upstream, RecognitionRatioSubstrateBlocker shows that a bare recognition ledger does not force the recognition-ratio law: the missing premise is a signed deficit-source constitutive coupling $c_\sigma=\kappa_\sigma\delta_\sigma$ linear in total strain inside the $J$-cost action. The ledger-energy bridge module supplies the corrected ledger-to-geometry map once that coupling is present.

This module is the R3 MODEL that adds the dual-entry column orientation. Strain is defined purely from integer debit/credit imbalance times magnitude; no field is an $x$-ratio or a real logarithm. The enrichment therefore stays inside the discrete ledger language while giving a concrete carrier for the missing constitutive source term.

Sibling objects include the dual-entry strain state, discrete carrier, cost-extension of the recognition ledger, enriched witnesses (with strain and zero-extract properties), the enriched witness ledger (with $\phi$-bound), equality-from-ledger, and the bare projection together with its non-injectivity and swap-even factorization facts.

proof idea

This is primarily a definition module. It introduces the dual-entry strain state and the maps that build an enriched ledger and project it to a bare ledger. Short lemmas record that the enriched witness recovers the intended strain, extracts zero when appropriate, stays within the $\phi$-absolute bound on the ledger side, and equals the of-ledger construction. The bare projection is shown not to be injective, and bare-factorable states are characterized as swap-even. No deep tactic scripts; the content is data layout plus elementary algebraic identities.

why it matters in Recognition Science

R3 is the enrichment step that makes the deficit-source constitutive coupling inhabitable. Downstream, RecognitionMeshDualEntryCoupling4D assembles banked R1 (mesh geometric deficit), R2 (mesh hinge kappa and source domination), and this R3 dual-entry strain state into a mesh dual-entry coupling, attacking the typed residual that the bare ledger cannot supply the constitutive source. The companion audit module requires headline theorems to print inside the standard axiom set.

The same enrichment is imported by Gap-2 kind-rule work, the gauge-counting inevitable-reasons census, and the gauge-history measure construction. Those modules need a richer posting-layer ledger than the bare substrate; dual-entry strain is the concrete MODEL that supplies signed imbalance without smuggling continuous ratio data. In the Seven Gaps program this closes the P2.1 terminal obstruction at the definition layer so later waves can prove, rather than assume, constitutive coupling.

scope and limits

used by (5)

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 (20)