Boundary-equivalence lemma for Boolean formula fragments

1 October 2026. Lean 4.30.0 kernel-checked formalization of the boundary-equivalence lemma in SAT boundary dynamics. The underlying relational and contextual-equivalence ideas are classical; novelty is not claimed.

The lemma in ordinary mathematics

Let B be a finite set of exposed Boolean variables. A fragment F(B,Y) is a finite Boolean formula with a finite set Y of existentially private variables. Define

$$R_F(a)\;\Longleftrightarrow\;\exists y\;F(a,y)=1.$$

A client can join fragments, introduce a fresh exposed variable, forget an exposed variable, permute exposed coordinates, and pin a coordinate to either Boolean value. Join always renames its two private namespaces apart. A client may use the input fragment repeatedly. Its observation is satisfiability.

Boundary-equivalence lemma. For every finite B and every pair F,G over B,

$$R_F=R_G \quad\Longleftrightarrow\quad \forall C\;[\operatorname{SAT}(C[F])\leftrightarrow \operatorname{SAT}(C[G])],$$

where C ranges over finite, well-typed clients using the operations above and fixed fragment constants. There is no bound on formula size, private-variable count, number of input occurrences or context depth.

The same equivalence holds for Boolean outcomes of finite adaptive clients that choose their next branch solely from a SAT answer. This is a semantic statement. It does not assert a cheap algorithm for constructing R_F or running a client.

For example, x and True are both satisfiable now. Pinning x to false separates them. In contrast, the closed private fragments y and not-y remain equivalent under every legal future client: each can choose its own private witness. Joining them remains satisfiable. Identifying their private witnesses would be a different, incorrect Join operation.

From definitions to the proof

The formal development begins with a finite Boolean formula syntax: variables, True, False, conjunction, disjunction and negation. Its evaluation is defined recursively. A fragment keeps this syntax; it is not defined to be its relation. Private namespaces are generated from the empty type, one point and disjoint sums. An enumeration theorem verifies their finiteness.

Each public operation acts on actual syntax. Its induced action on the relation is then proved:

Join uses tagged private-variable injections even when both operands are the same fragment. Forget moves the selected coordinate into a new private summand. Introduce does not reveal that hidden coordinate. Private alpha-renaming is also proved to preserve the relation.

Sufficiency. Induct on a typed client expression. Each constructor respects relation equality by the corresponding operation theorem. The Join case uses two induction hypotheses, so repeated uses of the input are covered. Equal final relations have equal nonemptiness, which is the SAT observation.

Necessity. For each assignment a to B, construct a client P_a that pins every boundary coordinate to its value in a. The formal separating-test lemma is

$$\operatorname{SAT}(P_a[F])\quad\Longleftrightarrow\quad R_F(a).$$

Thus equal observations for all clients imply agreement on every assignment. The empty boundary is included: the empty pin list is the identity test.

Adaptive extension. A finite decision tree asks SAT of a legal client expression and chooses one of two subtrees. Equal relations give equal query answers; induction gives equal Boolean outcomes. This proof is included in Lean, not merely asserted as an informal consequence.

A precise consequence for every exact summary

Let sigma map fragments to any mathematical summary type S. Call it exact if whenever sigma(F)=sigma(G), all legal future SAT observations agree. Then

$$\sigma\text{ is exact} \quad\Longleftrightarrow\quad \exists d\;\forall F\;d(\sigma(F))=R_F.$$

This factorization theorem is also kernel checked. One possible propositional decoder is

$$d(s)(a)\;\Longleftrightarrow\; \exists F\;[\sigma(F)=s\ \land\ R_F(a)].$$

Exactness makes this unambiguous on attained summary values. Conversely, any such decoder ensures that equal summaries give equal relations and hence equal future observations. This says exactly what information a correct summary must retain. It does not supply an executable decoder, an efficient encoding, or a bound on access, allocation or update time. A summary may additionally retain syntax or other information.

What the kernel checked

Download the complete source package. The package uses only Lean’s bundled core and standard library, with no Mathlib dependency. Its six modules separate the claims:

The main general declarations are contextualEq_iff_boundary_eq, finite_boundary_contextualEq_iff_relEq, finite_boundary_adaptiveEq_iff_relEq, and exactSummary_iff_decoder, all in namespace FPRD.Boundary. These quantify over arbitrary finite widths; they are not a collection of finite test results.

Every module was compiled from source in a fresh temporary import directory with warnings treated as errors. The audited dependencies are only propext and Quot.sound, Lean’s standard proposition-extensionality and quotient-soundness foundations; some declarations need fewer. No admitted proof, sorryAx, custom axiom, or native_decide is used. These checks do not make Lean, its compiler, or the surrounding operating system infallible; they identify the actual proof and checking boundary.

See the recorded check output, verification manifest, and reproduction instructions. The source guard supplements kernel checking; it does not replace it.

Assumptions that the examples protect

The formal controls prove that fresh private copies and an aliased private witness give different SAT answers; that signed Pin distinguishes two currently satisfiable fragments; and that forgetting then introducing a coordinate does not expose the old private variable. Another theorem shows that an explicitly restricted positive-only client language cannot distinguish the chosen pair. That restricted language excludes arbitrary negative fragment constants, which could otherwise restore separation even without a negative-Pin constructor.

Different private syntax can have identical future observations. Consequently this equivalence does not identify stored graphs, formula texts, private-witness counts, memory addresses or timing. Such observations are outside the interface.

The concrete fragment syntax is general finite Boolean syntax. Class-specific predicates and preservation proofs for 3CNF, Horn, 2CNF or affine systems are not encoded here. Neither are their relation counts, the independent-fragment probe lower bound, the persistent Horn implementation or the scaffold/TM compiler. Their previous proof statuses remain unchanged.

Repeated input occurrences model retained-handle reuse semantically. An actual DAG evaluator, sharing costs and an imperative retained-store interpreter are not formalized. Adaptive clients have finite decision trees; the checked adaptive extension concerns their Boolean outcome relation, not an encoded trace semantics or nontermination. Syntax-inspecting or timing-sensitive clients are excluded.

Classical foundations and why this checkpoint matters

Conjunction, existential projection and signed unit selection are established constraint semantics. The proof method is compositionality plus a separating family of experiments. The behavioral perspective also occurs in classical residual and bisimulation theory; see Rutten’s Automata and Coinduction (1998), sections 2-4 and 7. His deterministic-automaton development is background, not an imported theorem establishing this typed binary-Join interface.

This is an elementary foundational lemma, not a principal research result. Its formalization supplies a concrete, inspectable contract: which objects we store, which operations can act on them, which observations matter, and exactly which semantic information suffices. It stabilizes a foundation for resource theorems. It does not turn semantic equivalence into a characterization of bounded persistent realization.

The subsequent composition-access audit checks the quantitative claim against its exact access model, actual input sizes and classical source. It supplies a matching persistent scan and closes that claim as a classical application. These written resource arguments are outside this Lean package; further mechanization is not being used as a substitute for additional mathematical content.