IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondScratch
Scratch workspace for Gap 2's J-diamond route: finite four-set intersection lemmas that probe whether the recognition cost J, read from ledger imbalance, can pin the three free posting rates. Gravity and ledger authors cite it when checking census-span geometry before a cleaned theorem. The file is exploratory finite combinatorics (decide emptiness and pairwise meets), not a finished uniqueness proof.
claimScratch development of the Gap-2 $J$-diamond: combinatorial facts on a four-element index set (left/right tetrahedron edges, empty and double intersections, literal four-fold meet, and a finite decision procedure) aimed at reading posting rates from the imbalance form of the recognition cost $J$.
background
Gap 2 (C2) concerns the recognition cost of a letter in context and the census span test. Upstream work reduced the measure to aggregate linearity by kind (fixed totals per kind equal a constant times that kind's count). The posting layer plus the gluing law then left the three rates entirely free.
The intended fix is to define the recognition cost $J$ of a letter from the imbalance structure already carried by the ledger, and to read the three rates off that $J$. In Recognition Science, $J$ is the unique cost forced by the composition law, classically $J(x)=(x+x^{-1})/2-1$. This module sits under Gravity / SevenGaps and imports the Ehrhart-span Gap-2 development as its sole dependency.
Sibling names in the file (SC4, left/right edge sets, empty and double intersections, a four-fold meet literal, and a Fin 4 decision helper) indicate a small diamond or tetrahedron of combinatorial constraints on a four-point index set, used as a scratch pad for span and incidence checks.
proof idea
This is a scratch module, not a single closed theorem. The argument shape is finite combinatorics on a four-element carrier: name left and right edge collections, prove selected intersections empty or two-element, record a literal four-fold intersection, and discharge propositional goals by decide on Fin 4. No global uniqueness or rate-fixing theorem is sealed here; the file stages local incidence lemmas that a later Gap-2 J-diamond theorem would assemble.
why it matters in Recognition Science
In the Seven Gaps gravity program, Gap 2 must turn free posting rates into quantities fixed by recognition cost. Upstream Gap2JEhrhartSpan frames the route: define $J$ from ledger imbalance and read the rates off its census span. This scratch file explores the diamond incidence geometry that would support that reading.
It currently has no downstream used-by edges, so it does not yet feed a parent theorem in the mirror. Its place is preparatory: close or discard the J-diamond combinatorics before promoting a cleaned lemma into the Gap-2 chain that aims to fix the three rates left free by posting-plus-gluing. Framework contact is the J-uniqueness landmark (T5) and the Recognition Composition Law, only insofar as those justify using $J$ as the cost that could pin the rates.
scope and limits
- Does not prove that J fixes the three posting rates.
- Does not state a finished Gap-2 uniqueness or census-span theorem.
- Does not connect diamond incidence to physical mass or G formulas.
- Does not discharge sorry-free parent results; used_by is empty.
- Does not replace Gap2JEhrhartSpan; it only imports and scratches beside it.