Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjection

show as:
view Lean formalization →

Typed classical-source interface on Loom configurations: a source map, a discovery-gate equality, and a flag for whether the reading ignores depth-two content. Gravity analysts use it to project configs to classical readings without identifying stress-energy. The module supplies depth-one, abelian, and depth-two instances plus equality/separation lemmas on configuration pairs AB and CD.

claimA classical source projection on Loom configurations consists of a source map extracting a classical reading, an equality relation $\mathrm{Equal}$ used by the discovery gate (default: propositional equality on the carrier), and a Boolean $\mathrm{factorsThroughAbelian}$ recording whether the reading ignores depth-two content. Depth-one and abelian projections agree on configuration pairs $AB$ and $CD$; the depth-two reading separates those pairs. Physical stress-energy identification is not a field of the structure.

background

Loom configurations carry layered content that can be read at different depths. Depth-one content is the abelian, first-order reading; depth-two content includes commutator-type data that can distinguish order-sensitive histories. The upstream separation package records when two readings agree or when one reading separates a pair of configs (every door has a key, with a master key that locks or opens uniformly).

This module packages that idea as a typed interface for classical sources in the gravity analysis stack. The structure exposes only the classical reading, the equality used by discovery gates, and whether the reading factors through the abelianization. Stress-energy identification is deliberately excluded from the interface so that geometric or holographic response theorems can attach their own physical map later.

Concrete instances include a depth-one source, an abelian source, and a depth-two reading, together with named projections that fix the equality and abelian-factorization flags.

proof idea

Primarily a definition module: it introduces the SourceProjection structure and the concrete depth-one, abelian, and depth-two instances. The load-bearing lemmas are pairwise comparisons on fixed configuration pairs AB and CD: depth-one and abelian projections are shown equal on those pairs, while the depth-two reading is shown to separate them. The argument is by direct evaluation of the readings on the named configs, using the separation vocabulary from Loom.Separation rather than a long tactic development.

why it matters in Recognition Science

Feeds the order-sensitive history response on the Freudenthal patch (OrderSensitiveHistoryResponse4D), which builds an edge-current response from the depth-two commutator reading of a Loom config—the same second-order content isolated by pair traces and holonomy expansion. That downstream module freezes claims G2/G3 of the order-sensitive gravity proposition plan; this interface is the typed seat for the classical reading those claims consume.

Also imported by ClassicalSourceProjectionAudit, which checks that load-bearing theorems report only the base triple propext, Classical.choice, Quot.sound (or a subset). In the broader RS gravity stack, the module keeps classical-source extraction honest: abelian projections cannot see order-sensitive depth-two data, so any holographic or stress-energy identification must be stated explicitly downstream rather than smuggled into the source map.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)