Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry

show as:
view Lean formalization →

Defines the discrete geometry of n independent binary distinctions: each channel sits on one of two sides, so configurations form the vertices of an n-cube. Introduces vertices, edges, 0- and 1-chains, boundary maps, and the identity d^{2} = 0. Downstream cubical and Δ-native analysis modules import this as the combinatorial substrate. Mostly definitional scaffolding with one algebraic identity for the boundary.

claimA configuration is a map from $n$ channels to sides $\{\pm 1\}$ (equivalently a vertex of the $n$-cube). Edges join configurations that differ in exactly one channel. The module supplies chain groups $C_0$, $C_1$, boundary operators $d_1$, $d_2$, and proves $d^2 = 0$, together with difference and vertex-indicator helpers on this geometry.

background

In the Primitive Recognition Calculus, recognition proceeds by binary distinctions: each independent channel is either on one side or the other. A configuration of $n$ such channels is therefore a point of ${\pm 1}^n$, the vertex set of the $n$-dimensional hypercube. Flipping a single channel defines an edge; the resulting 1-skeleton is the natural place to put discrete differentials and costs.

The module packages that geometry for later analysis. Sibling names indicate: Config (the $n$-tuple of sides), Vtx/Edge (combinatorial cells), chain spaces C0/C1, boundary maps d1/d2, a boundary_squared_zero identity, plus diff/vertexIndicator utilities. The local setting is foundational discrete structure, not continuum physics yet: the cube is the state space on which recognition increments and ledger updates will act.

This sits upstream of the cubical chain complex and of native $\Delta$ analysis used to control multi-channel defects in the forcing chain.

proof idea

Primarily a definition module: configurations, vertices, edges, chain groups, and boundary operators are introduced by construction on the $n$-cube of binary distinctions. The main nontrivial content is the chain-complex identity $d^2 = 0$ (boundary_squared_zero), proved by the usual cancellation on pairs of edge flips (order of two distinct channel flips commutes, so oriented boundaries cancel). Commutation lemmas for diff support that cancellation. No deep analytic argument lives here; later modules consume the types and the $d^2=0$ fact.

why it matters in Recognition Science

Multi-distinction geometry is the combinatorial backbone for recognition with several independent channels. It feeds three direct importers: CubicalChainComplex (builds the full cubical complex on this skeleton), DeltaNativeAnalysis, and DeltaNativeStrongClosure (native discrete-difference estimates and closure results on the same configuration space).

In the Recognition Science forcing picture this is the discrete stage on which period-$2^3$ octave structure and $D=3$ spatial forcing eventually sit: binary channels and their cube geometry are how multi-bit recognition is counted before continuum limits or J-cost calculus appear. Without a clean $C_\bullet$ and $d^2=0$ here, cubical and $\Delta$-native arguments have nowhere to land.

scope and limits

used by (3)

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

declarations in this module (16)