subset_product_hit_of_minimal
plain-language theorem explainer
A minimal visibility engine, carrying only a KTheta floor hypothesis and stable budget, guarantees an admissible hard gate c for any non-identity reciprocal n such that the subset product phase hit set for that n and c is nonempty. Number theorists building phase budget engines in Recognition Science cite this to link minimal inputs directly to phase hits. The proof is a term-mode wrapper that extracts the gate via hits_admissible_gate and converts the balanced-phase witness with subsetProductPhaseHit_of_hitsBalancedPhase.
Claim. Let engine be a minimal visibility engine (cost function, stable budget for non-identity reciprocals, and KTheta failure floor hypothesis). For any natural number $n$ satisfying the non-identity reciprocal condition, there exists a natural number $c$ such that $c$ forms an admissible hard gate and the subset product phase hit set for $n$ and $c$ is nonempty.
background
MinimalEngine is the structure holding a costOf map from naturals to naturals, a stable budget predicate for every non-identity reciprocal n, and a KThetaFailureFloorHypothesis for those n. The module repackages the bounded visibility engine by dropping the explicit visibility field and replacing it with the theorem hits_balanced_phase_of_floor_and_budget. NonIdentityReciprocal n identifies n as a non-identity reciprocal ledger in the phase budget setting.
proof idea
The term proof opens with classical, performs rcases on hits_admissible_gate engine hn to obtain the triple c, hc, hhit, then applies exact to the pair consisting of hc and the result of subsetProductPhaseHit_of_hitsBalancedPhase hhit.
why it matters
This result supplies the witness used inside phaseBudgetEngine to populate the bound field of PhaseBudgetEngine, satisfying the membership check by reflexivity. It completes the minimal-engine repackaging step that feeds the Recognition Science phase-budget construction and the downstream Erdos-Straus residual extraction. The declaration sits at the interface between the KTheta floor hypothesis and explicit phase hits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.