HorizonPatchClassTarget
plain-language theorem explainer
Specification of a horizon patch class: a level-indexed microstate count that is everywhere positive and obeys the exact Fibonacci recurrence count(n+2)=count(n+1)+count(n). Horizon and gravity workers on the φ-absorption comb preflight cite it as the open P2 interface. It is a structure definition only; no derivation is claimed, and RS capital does not yet construct any instance from ledger or voxel data.
Claim. A horizon patch class target is a map $m:\mathbb{N}\to\mathbb{N}$ such that $m(n)>0$ for every $n$, and $m(n+2)=m(n+1)+m(n)$ for all $n$.
background
Module context is the Seven Gaps Pillar 3 fallback: a falsifier-gated preflight of a model φ-horizon absorption comb. Nothing here is a prediction. The candidate mechanism posits horizon area quantization with gap $\Delta A=4\ln(\varphi),\ell_P^2$, converting via black-hole thermodynamics into a repeated absorption comb at $GM\omega_*=\ln(\varphi)/(8\pi)\approx 0.019147$ for Schwarzschild. Load-bearing hypotheses are not derived from RS capital.
Existing capital supplies continuous horizon area $A=4\pi R_s^2$, a real capacity bound $A/\ell_0^2$, and a real-valued recognition ledger with boundary cost on a substrate bipartition. None of these quantize area or produce a discrete microstate spectrum. The sealed entropy identity $S=N/4$ is definitional, not a counting theorem.
The Fibonacci sequence (1,1,2,3,5,...) appears elsewhere in the stack as a named sequence; the open question is whether any horizon patch state type forced by ledger or voxel capital, after automorphism quotient, yields exactly that recurrence.
proof idea
No proof body: this is a structure bundling three fields. The first is a level-indexed natural-number count. The second asserts positivity at every level. The third asserts the two-step linear recurrence that the φ-comb algebra needs. Downstream code supplies instances by filling the fields; the structure itself only names the interface.
why it matters
This is the P2 open target in the horizon-ledger preflight. Doc-comment is explicit: no RS capital constructs it yet. A real derivation would need a forced horizon patch state type, an automorphism quotient, and a counting theorem.
It is consumed by the consistency witness that plugs in $\mathrm{Nat.fib}(\cdot+1)$ by fiat (showing the specification is satisfiable, not vacuous) and by the horizon comb model, whose IF-side requires a discrete patch class together with an inserted Fibonacci identification and a positive Planck-area bookkeeping constant. Entropy is then read as log-count and area as $4\ell_P^2 S$.
Pillar 3 stays open. The kinematic algebra and one asymptotic entropy-gap fact are real capital; quantization is not forced, and the P1 scaling falsifier already blocks a uniform ledger gap at the present formalization level. This structure isolates exactly the missing discrete counting step so the comb chain can be stated without pretending the gap is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.