An observer-consistency framework for physics with 639 Lean-checked results

berndtzl1 pts0 comments

observer-patch-holography/docs/HACKER_NEWS_START_HERE.md at main · FloatingPragma/observer-patch-holography · GitHub

//blob/show" data-turbo-transient="true" />

Skip to content

Search or jump to...

Search code, repositories, users, issues, pull requests...

-->

Search

Clear

Search syntax tips

Provide feedback

--><br>We read every piece of feedback, and take your input very seriously.

Include my email address so I can be contacted

Cancel

Submit feedback

Saved searches

Use saved searches to filter your results more quickly

-->

Name

Query

To see all available qualifiers, see our documentation.

Cancel

Create saved search

Sign in

//blob/show;ref_cta:Sign up;ref_loc:header logged out"}"<br>Sign up

Appearance settings

Resetting focus

You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.

Dismiss alert

{{ message }}

Uh oh!

There was an error while loading. Please reload this page.

FloatingPragma

observer-patch-holography

Public

Notifications<br>You must be signed in to change notification settings

Fork<br>72

Star<br>560

FilesExpand file tree

main

/HACKER_NEWS_START_HERE.md

Copy path

Blame<br>More file actions

Blame<br>More file actions

Latest commit

History<br>History<br>History

143 lines (117 loc) · 7.01 KB

main

/HACKER_NEWS_START_HERE.md

Copy path

Top

File metadata and controls<br>Preview

Code

Blame

143 lines (117 loc) · 7.01 KB

Raw<br>Copy raw file<br>Download raw file

OutlineEdit and raw actions

Start Here: The Skeptical Technical Entry Point

Observer Patch Holography asks whether public physics can be reconstructed<br>from finite observers that compare overlapping records and repair<br>disagreement.

This repository contains:

a sorry-free Lean 4 library of 639 checked theorems and lemmas, each public<br>theorem carrying a per-theorem axiom report;

reproducible finite simulations with an adversarial negative control;

machine-certified interval and uniqueness certificates for the declared<br>numerical maps;

an explicit list of open proof and physical-construction gaps.

Nothing here asks you to accept the full theory before checking an artifact.<br>Start with one theorem, one receipt, or one counterexample.

The Hypothesis In Two Sentences

Objective reality is modeled as the fixed point of finite observer patches<br>that keep records, compare them on overlaps, and repair disagreement until the<br>same record is recoverable from either side. The claim under test is that<br>spacetime signature, gauge structure, and specific dimensionless constants are<br>forced by that consistency requirement, on stated premises, without a table of<br>adjustable constants.

Three Things You Can Check

1. Build the Lean library

Requires elan; the toolchain is pinned<br>in Lean/lean-toolchain.

cd Lean<br>lake exe cache get<br>lake build

The library build is the proof receipt. Coverage and premises are indexed in<br>Lean/ObserverPatchHolography/PROOF_INDEX.md.<br>Continuum geometry, asymptotic tails, and physical identification are explicit<br>premises, stated as such in Lean/README.md.

2. Reproduce one numerical certificate

The pixel closure $P=\varphi+\sqrt\pi/A_T(P)$ is claimed to have exactly one<br>fixed point per declared map on the declared domain. The certificate is<br>interval arithmetic, so a failure is a hard failure.

python -m venv .venv && . .venv/bin/activate # CPython 3.12+<br>pip install -r requirements.txt<br>cd code/P_derivation<br>python3 global_uniqueness_certificate.py --mp-dps 40 --iv-dps 40 \<br>--su2-cutoff 120 --su3-cutoff 90 --initial-pieces 256<br>python3 -m pytest test_global_uniqueness_certificate.py -q

The gauge-width root sits $2.5\times10^{-6}$ from the measured<br>$\alpha^{-1}=137.035999177(21)$. The remaining gap has a stated address, the<br>open hadronic transport term; see<br>code/P_derivation/README.md for the claim<br>boundary.

3. Run the finite core and one negative control

From the repository root, with the same virtual environment:

python tools/check_claim_registry.py<br>python3 -m pytest -q \<br>code/a5_closure/test_audit.py \<br>code/capacity_readback/test_correctable_public_record_capacity.py \<br>code/capacity_readback/test_reversible_public_checkpoint_packet.py \<br>code/consensus/test_reference_architecture_benchmark_suite.py \<br>code/consensus/test_verified_tree_packet_net.py<br>python3 code/particles/calibration/strict_one_loop_pole_map/run_all.py

The last command regenerates a conditional receipt, runs its adversarial<br>suite, validates both JSON Schemas, and checks the receipt without importing<br>the producer. The simulation negative control lives in<br>evidence/einstein_convergence: at<br>constant coupling density the held-out event form carries Lorentzian signature<br>$(1,3)$ at 16k, 65k, and 262k carriers with the cone margin halving per rung,<br>and the density-starved control run degrades the signature to $(2,2)$ on cue.<br>Every stored number is sha256-bound and regenerates bit for bit...

code lean observer file search patch

Related Articles