module module moderate

`IndisputableMonolith.Loom.Separation`

Module packaging the Loom separation witness: two relational claims that differ only in quantifier order (every-door-some-key versus some-key-every-door) weave to configurations in distinct gauge orbits. Gravity analysts cite it when a classical source reading must be proved equal only on already-separated configs. The argument is a concrete certificate-backed pair of readings plus the shared codebook names.

claimThere exist two Loom contents $C_{\forall\exists}$ and $C_{\exists\forall}$ (every door opened by some key, versus some key that opens every door), built from shared names door, key, opens, locks, such that their weaves lie in different gauge orbits, while the two readings are genuinely distinct claims (not merely distinct syntax trees).

background

Loom turns relational content into configurations of closed walks. Grammar supplies the inductive type of content and the total map weave that sends content to a configuration via five production rules forced by algebraic properties of the operators. Semantics insists that "different content" means different claims, not just different trees: a pair that differs syntactically but agrees as claims would be an embarrassment rather than a witness.

Readings defines the rival side of the separation claim. Two honest shapes of a relational message appear: a ground bag (multiset of typed tuples over shared vocabulary, as an ingest contract carries) and a second reading of the same shape. The separation theorem is a claim about a rival, so that rival is fixed in Lean rather than left in a Python script.

CertificateData holds the measured certificate: a homomorphism from the free group of rank five into $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ found by search, together with automorphism tables for $Q_3$. The four shared names (door, key, opens, locks) are codebook indices into that vocabulary.

proof idea

Definition-and-witness module, not a single theorem wrapper. It names the shared codebook indices, builds the two quantifier-order contents (every-door-some-key-opens versus some-key-every-door-opens, and the dual lock variants), and exhibits concrete readings and a certificate-backed configuration pair. Separation is then the statement that the two weaves are gauge-inequivalent while the readings remain distinct as claims under the semantics of Readings and Semantics. Downstream modules import the witness rather than re-deriving the pair.

why it matters in Recognition Science

Feeds the order-sensitive gravity stack. ClassicalSourceProjection requires that a classical source reading of a Loom config may stand in for the conventional-source half of the discovery discriminator only when the reading is already proved equal on gauge-separated configs; this module supplies that separation. OrderSensitiveHistoryResponse4D seats the depth-two commutator reading of a Loom config as the history-to-edge-current response on the Freudenthal patch (frozen claims G2/G3 of the Order-Sensitive Gravity proposition). Without a proved content-level separation, gauge inequivalence of utterances would be uninteresting: the language might be drawing a distinction the logic does not. The module closes that gap for the door/key quantifier-order pair.

scope and limits

Does not prove separation for arbitrary Expr pairs, only the door/key quantifier-order witness family.
Does not define weave, gauge action, or certificate search; those live in Grammar, Semantics, and CertificateData.
Does not itself construct classical source projections or 4D history responses.
Does not claim syntactic inequality alone implies distinct claims; semantics must still certify claim-level difference.

used by (2)

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

IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjection module_import
IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Loom.CertificateData module_import
IndisputableMonolith.Loom.Grammar module_import
IndisputableMonolith.Loom.Readings module_import
IndisputableMonolith.Loom.Semantics module_import

declarations in this module (60)

def door L52
def key L53
def opens L54
def locks L55
def cb L62
def opensKeyDoor L64
def locksKeyDoor L65
def everyDoorSomeKeyOpens L68
def someKeyEveryDoorOpens L70
def everyDoorSomeKeyLocks L72
def someKeyEveryDoorLocks L74
def witnessA L77
def witnessB L79
theorem weave_witnessA L84
theorem weave_witnessB L85
theorem wellFormed_A L88
theorem wellFormed_B L90
theorem base_ok L100
theorem tableOfSubst_ok L105
theorem autSubst_length L109
theorem autTables_eq L114
theorem depth_one_is_blind L122
theorem abelianised_is_blind L127
theorem depth_two_separates L130
theorem invariant_separates L133
def gaugeImage L145
theorem invariant_gaugeImage L149
def separatesEverywhere L160
theorem separates_everywhere L163
theorem no_gauge_image_of_A_is_B L169
theorem gauge_image_ne_B L177
theorem witnesses_separated L185
def cb2 L216
def opensDoorKey L218
def locksDoorKey L219
def someDoorLocksEveryKey L222
def someDoorOpensEveryKey L224
def everyDoorOpensEveryKey L226
def everyDoorLocksEveryKey L228
def witnessC L230
def witnessD L231
theorem weave_witnessC L233
theorem weave_witnessD L234
theorem witnessC_ne_witnessD L238
def witnessModel L250
theorem witnessC_and_D_are_different_claims L259
theorem witnessC_holds L263
theorem witnessD_fails L264
theorem groundBag_blind L268
theorem adjacencyBag_blind L274
theorem depth_one_is_blind2 L279
theorem abelianised_is_blind2 L282
theorem depth_two_separates2 L285
theorem wellFormed_C L288
theorem wellFormed_D L290
def separatesEverywhere2 L293
theorem separates_everywhere2 L296
theorem no_gauge_image_of_C_is_D L301
theorem gauge_image_ne_D L308
theorem witnesses2_separated L313