Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.FoldMomentNamingLink4D

show as:
view Lean formalization →

Closes the Arc-2 naming question between the geometric hinge fold and the hybrid moment in 4D: the factor-of-two gap is a coefficient mismatch, not a naming identification. Tags provenance of the hybrid and fold t11 orbits, proves they mismatch, and packages the naming-link closure as a definition-level equality at the witnesses. Cite when auditing whether fold and moment are the same object under different names.

claimIn 4D gravity analysis, the geometric hinge fold and the hybrid moment are not identified by naming: the exact factor-of-two gap between fold and dictionary coefficients is a numerical mismatch, not a renaming. Provenance tags for the hybrid and fold $t_{11}$ orbits disagree; the naming link is closed by definitional equality at the witness points.

background

Arc 2, step 8 (GeometricFoldVsDictionary4D) showed that the geometric hinge fold is not the banked dictionary: after step 7 pinned the Einstein-Hilbert TT second variation at $-(1/4)$ per unit Frobenius and momentum and Regge normalization $\rho = 1/2$, the dictionary's $-(1/8)$ is the second variation of the Regge action, and the gap between fold and dictionary is exactly two. That closed the coefficient question and said nothing about what the tree's convergence theorem actually converges to.

This module sits one step downstream. It separates coefficient arithmetic from object identity: whether fold and hybrid moment are the same named quantity under different labels. Sibling declarations introduce provenance tags for the hybrid and fold $t_{11}$ orbits, a mismatch lemma between those tags, and an explicit witness that the factor-of-two gap is not a naming link. Closure is then packaged as definitional equalities (at witnesses and in the abstract).

proof idea

Definition-and-status module rather than a deep derivation. Provenance tags (hybrid vs fold $t_{11}$) are introduced as discrete labels; mismatch is by direct inequality of those tags. A dedicated lemma records that the factor-two witness does not constitute a naming identification. Naming-link closure is then stated three ways: as a definition, as equality of that definition to its expanded form, and as the same closure evaluated at the witnesses, each with a matching _eq form. A final status flag records step-9 task-1 completion. No heavy analytic machinery; the argument is bookkeeping that prevents reading the coefficient gap as an identity of objects.

why it matters in Recognition Science

Prevents a common misreading of Arc 2 step 8: that the exact factor-of-two between geometric fold and dictionary means fold and moment are the same object under two names. Downstream gravity analysis that consumes fold or moment coefficients needs a clean separation between numerical gap and naming. The module feeds the step-9 task ledger (step9_task1_status) and freezes the naming-link question so later 4D gravity theorems can cite a closed definition rather than reopen provenance. Within Recognition gravity, this keeps the geometric hinge analysis honest about what converges: coefficients match up to two; the named objects remain distinct unless a separate identification is proved.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)