pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Complexity.BalancedParityHidden

show as:
view Lean formalization →

This module defines the hidden mask encoder for bits in Boolean circuit models within Recognition Science. A bit b with mask R encodes as R when false and negation of R when true. Researchers examining the P versus NP gap via J-cost gradients in SAT would cite these primitives for circuit ledger constructions. The module consists solely of supporting definitions with no theorems or proofs.

claimThe hidden mask encoder for bit $b$ and mask $R$ is $R$ when $b=0$ and $R^c$ when $b=1$.

background

Recognition Science measures complexity through J-cost on the phi-ladder, with SAT instances resolved by the operator R̂ reaching zero cost in O(n) steps for satisfiable cases. This module supplies auxiliary Boolean encoding definitions that support modeling circuits as restricted sub-ledgers. It imports only Mathlib and introduces siblings such as enc, restrict, and extendMask to handle hidden parity masks for true/false bits.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed CircuitLedger for Boolean circuits as restricted sub-ledgers and RSatEncoding for the R̂ SAT claim that satisfiable k-CNF instances reach zero J-cost in O(n) recognition steps. They also support ComputationBridge and Core.Complexity explorations of whether feed-forward circuits can simulate the global J-cost gradient used by R̂.

scope and limits

used by (4)

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

declarations in this module (12)