@@ -0,0 +1,196 @@
+# arXiv:2408.10592 — Hologram is a graph: theorems need matched witnesses
+
+**Paper:** Litian Huang, Xinguo Yu, Feng Xiong, Bin He, Shengbing Tang, Jiawen Fu (2024), *Hologram Reasoning for Solving Algebra Problems with Geometry Diagrams*  
+**Primary source:** https://arxiv.org/abs/2408.10592  
+**PDF:** https://arxiv.org/pdf/2408.10592  
+**Author code:** https://github.com/FerretDoll/HGR  
+**Source inspected:** arXiv v1, 9-page PDF (20 August 2024); method pp. 3–5; tables 1–3 p. 7; limitations p. 8 (PDF pages counted from 1).  
+**Status:** SOURCE EXTRACTION + PROPOSED LANCE-GRAPH FALSIFIERS; no code port, benchmark or parity result implied.
+
+## Punchline
+
+> **Keep observations addressable; let theorems be independently declared consumers of the same graph. A fast candidate mask is not a proof: pattern binding and its constraints must still pass.**
+
+This paper's word *hologram* denotes a **heterogeneous attributed geometry graph**, NOT HRR/FHRR, a phase-bound VSA, or distributed bit-vector superposition. Its real contribution is to make a collection of theorem templates reusable over a shared graph representation and to improve the *choice* of which template to attempt.
+
+Portable separation:
+
+~~~text
+text + diagram
+     ↓ parse (may be wrong)
+graph G = primitives + relations + mathematical and visual attributes
+     ↓ select theorem candidate (policy is a heuristic)
+match pattern under structural constraints
+     ↓ enforce mathematical and visual constraints
+       ├─ proving model: derive relationship ΔG
+       └─ property model: derive equations E
+     ↓ solve equations / update derivation state
+explicit theorem + operands + relation + equation + answer
+~~~
+
+No unvalidated visual resemblance may silently become a mathematical theorem.
+
+## Paper extraction: concrete mechanism
+
+### H1. One global geometry graph with distinct attribute kinds (paper §Method / Hologram; PDF p. 3)
+
+Paper notation: \`G=(V,E,A,Â)\`.
+
+- \`V\`: points, lines, angles, arcs, circles, polygons.
+- \`E\`: geometric relations (incidence, adjacency, perpendicularity, parallelism, congruence, similarity). HGR uses an **undirected** graph for these relations.
+- \`A\`: measured / mathematical values including lengths, angles, areas and target attribute \`τ\`.
+- \`Â\`: diagram-derived visual cues such as approximate positions, apparent lengths and apparent angles. The paper explicitly excludes these from formal calculation; they help disambiguate candidate matches.
+
+The same \`G\` is read by distinct operations; the distinction between admissible mathematical facts and visual hints is a useful cross-consumer boundary.
+
+### H2. Theorem templates are first-class models (paper §Graph Model Construction; PDF pp. 4–5)
+
+There are two kinds of templates:
+
+~~~text
+proving model  M_prov = (G_p, R, Ĉ, C, ΔG)
+property model M_prop = (G_p, R, Ĉ, E)
+~~~
+
+- \`G_p\` is an attributed-agnostic *pattern graph* (for structural matching).
+- \`R\` is a readable relation template for the resulting explanation, not a freely inferred fact.
+- \`Ĉ\` denotes visual constraints used to resolve potential pattern ambiguity.
+- \`C\` denotes mathematical preconditions of a proving model.
+- \`ΔG\` introduces derived vertices, edges or attributes after proof.
+- \`E\` denotes equations a property model can generate.
+
+Proving a relationship and using an already-established relationship to form an equation are different operations. HGR's example first proves parallelism, then applies the parallelogram property.
+
+### H3. Structural matching is VF3, not a mere bitmap intersection (paper §Model Matching; PDF p. 5)
+
+Paper matcher seeks a mapping \`M: V_p → V_g\` preserving the graph's required structure and edge/non-edge relationships; the implementation uses VF3.
+
+After finding a mapping, HGR evaluates each mathematical constraint against the mapped primitives, then checks auxiliary visual constraints. Only successfully matched models may produce their outcomes.
+
+**Substrate distinction:** \`R = P_a & P_b & aperture\` can prune candidate addresses. It cannot *alone* certify a multi-vertex graph match, variable binding, required edge presence/absence, or numeric constraints. Any RelAlg / Datalog / Quack / R2IL lowering must preserve all of these.
+
+### H4. Iterate derivation, not just retrieval (paper §Reasoner; PDF pp. 5–6)
+
+A successful proving model produces \`G' = G + ΔG(M(V_p))\`. A successful property model adds instantiated equations to \`E_total\`. The solver evaluates \`E_total\`, updates available mathematical attributes, and repeats until target \`τ\` is reached.
+
+Graph Transformer embeddings encode current graph state for a DQN theorem-choice policy; they do not replace VF3 matching or numerical theorem checks. Learned scheduling and mathematical validity are different layers.
+
+### H5. Study scale and measured claims (paper §Implementation / §Evaluation; PDF pp. 6–7)
+
+- Geometry3K has **3,002** multiple-choice geometry problems, with text, diagram and parsing annotations.
+- Model pool: **13 proving** plus **51 property** models (64 total).
+- The paper's accuracy metric chooses the nearest multiple-choice answer to the solver's numeric output; when no output is produced, a random choice is made. Thus it is not a formal-proof-success rate.
+- HGR overall accuracy: **68.7%** using its parser; **89.6%** using ground-truth (GT) parsing. Do not report 89.6% as end-to-end.
+- With GT: GeoDRL baseline **89.4%**, Inter-GPS **78.3%**.
+- With GT: HGR averages **2.26 theorem applications**, **7.29 relations**, **17.55 equations** per solved problem (Table 2).
+- HGR uses a Graph Transformer + DQN theorem selector, pre-trained with heuristic/random selection samples. These components optimize search order, not the semantics of rules.
+
+Ablation with GT parsing (paper Table 3, PDF p. 7):
+
+| Configuration | Overall accuracy |
+|---|---:|
+| HGR complete | 89.6% |
+| Without theorem-selection agent | 83.4% |
+| Without proving models | 79.5% |
+| Without property models | **27.0%** |
+| Without mathematical constraints \`C\` | 73.6% |
+| Without visual constraints \`Ĉ\` | 63.1% |
+
+**Interpretation:** A theorem pool, formal applicability constraints, and rules that produce equations are consequential. The strongest ablation is property models, but percentages alone do not identify any improvement in the proposed lance-graph executor.
+
+### H6. Known boundaries (paper §Failure Case; PDF p. 8)
+
+The published system fails on tasks requiring auxiliary geometric constructions and some shaded-region area calculations. Finite prepared-theorem coverage is a limitation. A new theorem template is not equivalent to the ability to invent new mathematics.
+
+## Extraction → lance-graph design (our engineering hypotheses, NOT paper claims)
+
+### L1. Reuse a typed theorem consumer over canonical graph observations
+
+~~~text
+Observed geometry (immutable, source-positioned)
+    ↓ ClassView / typed primitive and relation reading
+Candidate theorem
+    ↓ symbolic simplification and presence masks
+Bound graph match
+    ↓ structural + numerical preconditions
+Derived theorem witness + equations
+    ↓ separate derived generation / virtual branch
+Replayable proof / answer
+~~~
+
+Suggested logical representation; do not introduce new stored structs until a falsifier proves existing ClassView/SoA/Quack machinery insufficient:
+
+~~~text
+TheoremTemplate {
+    pattern: typed relation predicates,
+    required_edges: declared,
+    prohibited_edges: declared,
+    math_checks: exact or tolerance-typed predicates,
+    visual_hints: candidate-ranking ONLY,
+    conclusion: derivation recipe,
+    explanation: operand-bound template
+}
+~~~
+
+The source paper does not propose HHTL, SoA, masks, CE64, NAL or R2IL.
+
+### L2. Visual/heuristic evidence cannot certify the theorem
+
+\`Â\` can prioritize a match, but a proof certificate must be based on authorized structural/mathematical conditions. Example: two diagram lines *looking* parallel does not establish parallelism.
+
+This is analogous to \`Primed != Attended != Proven\`, but HGR itself does not define those categories.
+
+### L3. Preserve derivation provenance when updating a graph
+
+The paper updates its problem-local \`G\` in place. A replayable substrate can instead retain:
+
+~~~text
+input_version
+theorem_model_id + theorem_model_version
+bound_vertex_addresses / role assignments
+source relation witnesses
+structural and mathematical check results
+derived_relation_or_equation
+output_generation
+~~~
+
+The expansion \`ΔG\` should be a **derived view or explicitly committed version**, never indistinguishable from the original diagram observations.
+
+### L4. Theorem selector is not the theorem executor
+
+For a fair comparison: hold exactly the same 64 models, theorem constraints, equation solver and parse output fixed; change *only* the candidate selection / execution path. Compare a heuristic model selector, HGR DQN (if reproducible), and optional information-gain scheduling separately.
+
+### L5. R2IL lowering has to preserve joins and graph isomorphism checks
+
+Mask-first candidate pruning may reduce loads; it is not a proof of VF3 parity. Multi-entity binding, edge labels, required absences, symmetry and numerical checks all need independently executable oracles.
+
+No claim of O(1) end-to-end VF3 elimination, no claimed speedup, and no speculative benchmark number.
+
+## Executable falsifier matrix (proposed, NOT SHIPPED)
+
+| ID | Experiment | Pass criterion | Falsifier |
+|---|---|---|---|
+| HGR-F01 | Port a tiny, explicit theorem pool: parallelism and parallelogram side relation | Same admissible matches and instantiated equations as trusted VF3 + reference numeric checker | Candidate masks report matches violating structural/math constraints |
+| HGR-F02 | Visual red herring: drawn parallel but no symbolic/numeric proof | No theorem-certified parallel relation merely from visual similarity | Visual cue upgrades guess to proven fact |
+| HGR-F03 | Proving vs property model separation | Proof conclusion and property equation appear in distinct provenance-qualified steps | Equation is emitted without the precondition or origin |
+| HGR-F04 | Same frozen graph, multiple legal lowerings | Identical bound match set, equations, terminal values and witness provenance | A lowering silently drops edge absence or argument bindings |
+| HGR-F05 | Replay a derivation on an immutable input version | Identical derived overlay; original graph byte-identical | Derived relation pollutes original observations |
+| HGR-F06 | Ordering/cost ablation against VF3 | Correctness parity first, then measure mask construction, candidate binds, scanned bytes, runtime | Speed claim based solely on candidate pruning, no full matching parity |
+| HGR-F07 | Novel problem requiring new auxiliary construction | Explicitly report unsupported template/construction | Unsupported branch silently fabricates theorem applicability |
+
+## Relation to arXiv:2606.24948
+
+Read alongside [2606.24948](2606.24948_superposition_capacity_breaks_two_hop_retrieval.md). The same word “hologram” hides two different architectures:
+
+- 2408.10592: an explicitly attributed geometry graph plus theorem-pattern operations.
+- 2606.24948: superposed HRR/FHRR vectors queried by approximate unbinding.
+
+They cannot be ranked from reported accuracy alone: Geometry3K equation-solving with explicit theorems and FB15k-237 zero-shot link composition are different tasks.
+
+## Scope and evidence boundary
+
+**Directly extracted from paper:** geometry graph type, two theorem kinds, VF3/constraints, DQN policy, Geometry3K numbers, limitations.  
+**Proposed by us:** HHTL address mapping, replay certificates, RelAlg/Datalog/Quack lowering, R2IL/mask-risc, CE64/admissibility, falsifiers.  
+**Not tested here:** HGR reproduction, code import, solver correctness, mask-read latency, benchmark parity, neural policy transfer.
+
+**One-line criterion:** *A theorem is reusable because its applicability can be tested on newly bound evidence, not because a candidate resembles the theorem's picture.*