Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D

show as:
view Lean formalization →

Finite 4D order-sensitive history response on the Freudenthal sixteen-site patch: antisymmetric seating, first-variation edge currents, and response differences that separate ordered Loom histories from classical metric strain. Gravity analysts cite it as the discrete gate before continuum residual promotion. The module defines fingerprints, seat generators, Dirac probes, and forward/reverse response lemmas used by the residual and audit layers.

claimOn the sixteen-site Freudenthal patch with Q3 seating (spatial axes in bits $0,1,2$, record-time in bit $3$), an antisymmetric edge generator induces a first-variation edge current (history response) for an ordered classical source pair. The forward-minus-reverse response difference is the finite order-sensitive residual, to be tested against linearized metric edge images $F$ arising as strain currents of $\mathrm{Mat}_4$ perturbations.

background

This module is the finite history-response layer of the Order-Sensitive Gravity proposition (frozen worlds G0/G1 and metric-null). Upstream, a classical source projection is a typed reading of a Loom Config allowed to stand in for the conventional-source half of the discovery discriminator, only when already proved equal on the gauge-separated quotient. Q3 patch seating packs Pattern-3 axes into bits 0,1,2 and record-time into bit 3 on the Fin-16 patch, without pulling the heavy gravity chain.

MetricEdgeImage F means $F$ is the strain current of some $\mathrm{Mat}_4$ perturbation on that patch; the strain formula and binary coordinates match the Freudenthal cover edge-current action. Loom separation supplies the kernel-checked witness that distinguishes legitimate one-way key/door structure from its security dual, used here to keep gauge-equivalent readings from contaminating the residual test.

Sibling objects include a polynomial fingerprint of natural-number lists, unit weights, Dirac probes on edges, seat generators, antisymmetric edge data, history response, response difference, and the first variation of the edge current.

proof idea

Definition-and-lemma module, not a single theorem. It introduces list fingerprints, antisymmetric edges, a distinguished seat generator, history response, response difference, edge-current first variation, Dirac probes, and unit weight. Short lemmas record that the seat generator is nontrivial, that antisymmetry flips under edge reversal, and that the forward history response is the corresponding first-variation evaluation. Downstream continuum and audit modules import this package as the finite gate; no continuum limit or trichotomy is proved here.

why it matters in Recognition Science

Parent consumers are the continuum order-sensitive residual (Campaign G4/G5) and the axiom audit for this module. The continuum layer replaces finite Boolean non-membership in MetricEdgeImage by a normalized-separation trichotomy under a shape-regular refinement family; it needs a clean finite residual built from ordered history response. The audit requires that the load-bearing finite gate report the base triple (or a subset) and reject silent sorryAx.

In the Recognition gravity stack this is the discrete witness that order of source seating is not absorbed by linearized metric strain on the eight-tick / D=3 Freudenthal patch. It sits between classical source projection, Q3 seating, and metric edge image on one side, and continuum residual promotion on the other, closing the finite half of the order-sensitive discriminator without yet claiming continuum separation.

scope and limits

used by (2)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (25)