hits_admissible_gate
plain-language theorem explainer
A minimal visibility engine produces an admissible hard gate for every non-identity reciprocal natural number. Number theorists working on phase budgets in Recognition Science cite this when deriving subset product hits solely from floor and budget data. The proof is a one-line term application of the balanced phase construction lemma to the engine's stable budget and K-theta floor hypotheses.
Claim. Let $E$ be a minimal visibility engine. For every natural number $n$ that forms a positive non-identity reciprocal ledger, there exists a natural number $c$ such that $c$ is an admissible hard gate and the pair $(n,c)$ satisfies the balanced residual phase condition for a square-budget divisor box.
background
The MinimalEngine structure consists of a cost function together with two hypotheses: a stable integer ledger budget for each non-identity reciprocal $n$, and a KTheta failure floor hypothesis for the same $n$. NonIdentityReciprocal $n$ requires $n>0$, $n≠1$, and the existence of $N$ such that $n$ divides $N^2$. HitsBalancedPhase $n c$ asserts the existence of a divisor exponent box where the reciprocal defects land in phase $-N$ modulo $c$ with the stated divisor conditions on $N+d$ and $N+e$ for the box divisors $d,e$.
proof idea
The proof is a direct term application of hits_balanced_phase_of_floor_and_budget to the three arguments hn, engine.stable n hn, and engine.floor n hn. No additional tactics or reductions are performed.
why it matters
This theorem supplies the admissible gate witness required by the downstream result subset_product_hit_of_minimal, which converts the gate into a SubsetProductPhaseHit. It closes the visibility field into a theorem inside the minimal engine, completing the repackaging step described in the module doc-comment and feeding the number-theoretic layer of the Recognition Science forcing chain at the level of Erdos-Straus rotations and balanced phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.